Es una generalización de una analogía sintáctica entre varios sistemas de la lógica formal y varios cálculos computacionales que fue descubierta por primera vez por Haskell Curry y William Alvin Howard.En particular, se divide en dos correspondencias.Una al nivel de fórmulas y tipos que es independiente de qué modelo de computación se esté usando; y otra al nivel de demostraciones y programas que es específica a una elección particular de modelo de computación y sistema lógico.A nivel de fórmulas y tipos, la correspondencia dice que la implicación se comporta de la misma manera que el tipo de las funciones entre dos tipos, que la conjunción se comporta igual que el producto de tipos (la tupla de dos tipos) y la disyunción igual que el tipo suma (llamado tipo unión en ocasiones).La fórmula verdadera se comporta como un tipo singleton mientras que la fórmula falsa lo hace como un tipo vacío, que no tuviera instancias.
Una demostración escrita en forma de programa funcional: la demostración de la conmutatividad de la suma de números naturales en el asistente de demostraciones
Coq
.
nat_ind
representa la
inducción matemática
, mientras que
eq_ind
representa la sustitución entre iguales y
f_equal
la congruencia de la igualdad respecto a la aplicación de una función a ambos lados de la misma. Varios teoremas anteriores que muestran que
m
=
m
+ 0 y S (
m
+
y
) =
m
+ S
y
son referenciados en la demostración.
