À l'aide de la machine de Krivine (une machine abstraite avec pile et environnement pour le lambda-calcul), on montrera comment il est possible de compléter le lambda-calcul avec des primitives de contrôle (exceptions, call/cc, ...), ce qui mène très directement au lambda-mu calcul de Parigot. On introduira ensuite les règles de typage du lambda-mu calcul, ce qui permet d'étendre la correspondance de Curry-Howard à un cadre classique et d'analyser le non déterminisme de la logique classique de Gentzen (LK). On obtient alors des systèmes logiques prouvant les mêmes formules que LK mais dont l'élimination des coupures a une interprétation calculatoire précise.
Publié le : 2002-07-05
Classification:
isomorphisme de Curry-Howard,
instructions de contrôle,
logique classique,
déduction naturelle,
lambda-mu calcul,
machine de Krivine (KAM),
lambda-calcul,
[MATH.MATH-LO]Mathematics [math]/Logic [math.LO],
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
@article{hal-00003753,
author = {Laurent, Olivier},
title = {Interpr\'etation calculatoire de la logique classique via le lambda-mu calcul et la machine de Krivine},
journal = {HAL},
volume = {2002},
number = {0},
year = {2002},
language = {en},
url = {http://dml.mathdoc.fr/item/hal-00003753}
}
Laurent, Olivier. Interprétation calculatoire de la logique classique via le lambda-mu calcul et la machine de Krivine. HAL, Tome 2002 (2002) no. 0, . http://gdmltest.u-ga.fr/item/hal-00003753/