Loading [MathJax]/extensions/MathZoom.js
Lambda -mu calcul et dualité, appel par nom et appel par valeur
Rocheteau, Jérôme
HAL, hal-00003547 / Harvested from HAL
Text on HAL
L'extension à la logique classique de la correspondance de Curry-Howard permet d'envisager deux réductions déterministes qui correspondent, pour la première, à une réduction avec appel par nom et, pour la seconde, à une réduction avec appel par valeur. On étudie cette dualité, d'une part à travers le lambda-mu calcul dont les réductions reposent sur la distinction fonction/argument de la déduction naturelle, et d'autre part à travers le lambda-mu-mu-tilde calcul dont les réductions reposent sur une symétrie gauche/droite du calcul des séquents. On montre des théorèmes de simulation entre le lambda-mu calcul et le lambda-mu-mu-tilde calcul qui respectent le mécanisme d'évaluation (cbn/cbv).
Publié le : 2002-09-25
Classification:  simulation,  appel par nom,  appel par valeur,  lambda-mu calcul,  déduction naturelle,  calcul des séquents,  [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] 
@article{hal-00003547,
     author = {Rocheteau, J\'er\^ome},
     title = {Lambda -mu calcul et dualit\'e, appel par nom et appel par valeur},
     journal = {HAL},
     volume = {2002},
     number = {0},
     year = {2002},
     language = {fr},
     url = {http://dml.mathdoc.fr/item/hal-00003547}
}

Rocheteau, Jérôme. Lambda -mu calcul et dualité, appel par nom et appel par valeur. HAL, Tome 2002 (2002) no. 0, . http://gdmltest.u-ga.fr/item/hal-00003547/