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:18] apeiron [Réalisabilité classique] |
fr:research:archives [2018/03/29 15:20] apeiron [Réalisabilité classique] |
||
|---|---|---|---|
| Ligne 41: | Ligne 41: | ||
| {{ :fr:research:realizability_in_classical_logic.pdf |son article}} traitant de réalisabilité classique. | {{ :fr:research:realizability_in_classical_logic.pdf |son article}} traitant de réalisabilité classique. | ||
| + | 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. | ||
| ====== Projets de thèse ====== | ====== Projets de thèse ====== | ||