Différences
Ci-dessous, les différences entre deux révisions de la page.
| Les deux révisions précédentes Révision précédente | Prochaine révision Les deux révisions suivantes | ||
|
fr:research:archives [2018/03/29 15:20] apeiron [Réalisabilité classique] |
fr:research:archives [2018/03/29 15:24] apeiron [Réalisabilité classique] |
||
|---|---|---|---|
| Ligne 43: | Ligne 43: | ||
| La logique intuitionniste peut être vue comme la logique classique où des règles équivalentes comme le tiers exclu, l'élimination de la double négation ou la loi de Peirce ne seraient plus toujours autorisées. La correspondance de Curry-Howard permet d'associer à chaque preuve en logique intuitionniste un programme en lambda-calcul. En cherchant à typer une instruction de contrôle dans un langage dérivant du lambda-calcul, l'informaticien Tim Griffin associa un programme (la commande $\mathtt{callcc}$) à la loi de Peirce. | La logique intuitionniste peut être vue comme la logique classique où des règles équivalentes comme le tiers exclu, l'élimination de la double négation ou la loi de Peirce ne seraient plus toujours autorisées. La correspondance de Curry-Howard permet d'associer à chaque preuve en logique intuitionniste un programme en lambda-calcul. En cherchant à typer une instruction de contrôle dans un langage dérivant du lambda-calcul, l'informaticien Tim Griffin associa un programme (la commande $\mathtt{callcc}$) à la loi de Peirce. | ||
| + | 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é. | ||
| + | |||
| + | 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 ====== | ||