Correspondencia de Curry-Howard

En su forma más general, la correspondencia de Curry-Howard es una correspondencia entre sistemas formales de tipos para ciertos modelos de computación y ciertos sistemas formales de demostraciones. 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.

• Howard, William A. (Septiembre de 1980) [​manuscrito original del 1969​], «The formulae-as-types notion of construction», en Seldin, Jonathan P.; Hindley, J. Roger, eds., To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Boston, MA: Academic Press, pp. 479-490, ISBN 978-0-12-349050-6 ..