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 diferentes sistemas lógicos llamados “teoría de tipos” que buscaban dar un sistema formal para la lógica intuicionista. Una preocupación de Martin-Löf es construir un sistema que pueda ser un fundamento para la matemática y por lo tanto sustenta el sistema formal a través de las llamadas “explicaciones de sentido” (meaning explanations).
En esta charla haré un resumen de las explicaciones lógicas e introduciré (alguna versión de) teoría de tipos, espero mostrar también en qué sentido podemos descubrir un lenguaje de programación en la teoría de tipos.
(source)