El isomorfismo de Curry Howard establece una sorprendente correspondencia entre sistemas de lógica formal y cálculos computacionales. El isomorfismo adquiere distintas formas: las fórmulas se corresponden a tipos, las pruebas se corresponden a programas, la existencia de una prueba se corresponde a la existencia de un programa de cierto tipo, la normalización de pruebas se corresponde a la ejecución de programas, etc. En este seminario exploraremos algunos sistemas de lógica formal y cálculos computacionales y las correspondencias que surgen entre ellos.
(source)