Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

Les deux révisions précédentes Révision précédente
fr:research:archives [2018/03/29 15:24]
apeiron [Réalisabilité classique]
fr:research:archives [2018/03/29 15:27] (Version actuelle)
apeiron [Réalisabilité classique]
Ligne 45: Ligne 45:
 Ainsi, la correspondance de Curry-Howard peut être étendue à la logique classique. Plus formellement,​ étendons le lambda-calcul habituel avec une instruction cc pour << current continuation >> en introduisant des piles e termes clos et des continuations comme termes. Alors il est possible de définir un système de transition, qui est un lambda-calcul avec continuations. Ainsi, la correspondance de Curry-Howard peut être étendue à la logique classique. Plus formellement,​ étendons le lambda-calcul habituel avec une instruction cc pour << current continuation >> en introduisant des piles e termes clos et des continuations comme termes. Alors il est possible de définir un système de transition, qui est un lambda-calcul avec continuations.
  
-Jean-Louis Krivine va plus loin dans ce papier et les autres en associant des programmes aux axiomes de la théorie des ensembles et à l'​axiome du choix, ce qui permet d'​étendre la correspondance à tous les théorèmes prouvés depuis l'​antiquité.+Jean-Louis Krivine va plus loin dans ce papier et les autres en associant des programmes aux axiomes de la théorie des ensembles et à l'​axiome du choix, ce qui permet d'​étendre la correspondance à tous les théorèmes prouvés depuis l'​antiquité. Pour un résumé accessible de ses travaux, voir {{ :​fr:​research:​expose_krivine.pdf |l'​exposé de Krivine}} à un colloque de sciences cognitives.
  
 Cette approche très constructive stimula mon intérêt pour les modèles de calcul, notamment implémentés sous forme de système de transition comme ce fût le cas durant ma thèse, ainsi que pour la correspondance preuve-programme,​ notamment lors de mon apprentissage de Coq durant mon postdoc. Cette approche très constructive stimula mon intérêt pour les modèles de calcul, notamment implémentés sous forme de système de transition comme ce fût le cas durant ma thèse, ainsi que pour la correspondance preuve-programme,​ notamment lors de mon apprentissage de Coq durant mon postdoc.
 +
 +
 ====== Projets de thèse ====== ====== Projets de thèse ======