En un seminario anterior, Francisco Trucco presentó el isomorfismo de Curry-Howard y para ello introdujo el cálculo lambda. La noción de cómputo en el cálculo lambda es sintáctica y consiste en reducir paso a paso expresiones. En este seminario, presentaré…
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…
Miguel Pagano, 2016-05-04: “Introducción a la Teoría de Tipos”
Next Wednesday M. Pagano (FaMAF-UNC) will give us an introduction to the theory of types, which is relevant both for Math and Computer Science, foundationally and in applications. Título: Introducción a la Teoría de Tipos Resumen: Desde comienzos de los 1970 Per Martin-Löf propuso…