Isomorphisme de Curry-Howard
L'isomorphisme de Curry-Howard est une relation entre la logique mathématique et l'informatique, par l'intermériaire du lambda-calcul. En effet on peut voir le type d'une fonction comme une formule booléenne.
Par exemple en lambda calcul simplement typé, si on associe à chaque type de base une variable propositionnelle et que l'on associe l'implication logique au type 
alors l'ensemble des formules vraies correspond aux types des termes clos du lambda-calcul typé.
Par exemple pour la formule 
on peut construire le lambda-terme λxa.x
Par contre il n'y a pas de lambda terme clos pour la formule A car on ne peut que faire le terme xa mais ce n'est pas un terme clos vu que la variable x est libre.
Si on étend le lambda calcul au produit cartésien, on aura parallèlement le et logique. Si on rajoute la somme disjointe (types somme ou structures) on aura le ou logique. Dans les lambda-calculs d'ordre supérieurs on rajoute des variables de types donc des quantificateurs. Cela donne les pour tout.
Grâce à cet isomorphisme on peut prouver la consistance d'une logique en démontrant la normalisation forte du lambda-calcul associé. C'est ainsi que Jean Yves Girard a démontré la consistance de la logique intuitionniste du second ordre en démontrant la normalisation forte du Système F.
| Système fonctionnel | Système formel |
|---|---|
| Calcul des constructions (Thierry Coquand) | ? |
| Système F (Jean-Yves Girard) | Arithmétique de Peano du second ordre / Logique intuitionniste du second ordre |
| Système T (Kurt Gödel) | Arithmétique de Peano du premier ordre / Logique intuitionniste du premier ordre |
| Système T1 | ? |
| T0 (Récursion primitive) (Stephen Cole Kleene ? Thoralf Skolem ?) | Arithmétique primitive récursive |
| lambda-calcul simplement typé | Calcul propositionnel intuitionniste |
Un logicien français, Jean-Louis Krivine a fait le rapport entre différents théorèmes mathématiques et les programmes informatiques qu'ils représentent.
- l'absurde (appelé bottom :
) a pour lambda-terme λx.x, ce qui correspond à « pour tout x, x » c’est-à-dire que tout est vrai. Comme on utilise un système cohérent ceci est toujours faux. En informatiques celà correspond à une instruction d'échappement, d'exception.
- le théorème d'incomplétude de Gödel qui dit qu'il y a des théorèmes que l'on ne peut pas démontrer correspond à un programme de réparation de fichiers.
- le théorème de complétude de Gödel correspond lui à un désassembleur de programmes.