Francisco Trucco, 2019-10-02: “El Isomorfismo de Curry Howard”

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 correspondecias que surgen entre ellos.

Leave a Reply

Your email address will not be published. Required fields are marked *