Correspondencia de Curry-Howard
isomorfismo entre los programas de ordenador y las demostraciones matemáticas / De Wikipedia, la enciclopedia encyclopedia
En teoría de la demostración y teoría de lenguajes de programación, la correspondencia de Curry-Howard (también llamada isomorfismo de Curry-Howard) es la relación directa que guardan las demostraciones matemáticas con los programas de ordenador. 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.[1]