Introducción a la correspondencia pruebas-programas

Curso de posgrado, primer semestre de 2021, Facultad de Ciencias.

Horarios

Teóricos:
- Lunes, de 13:15 a 14:45 (por Zoom)
- Viernes, de 13:30 a 15:00 (por Zoom)
Práctico:
- Viernes, de 11:30 a 13:30 (por Zoom)

Diapositivas del curso

Principios del intuicionismo y del constructivismo (versión del 15/03/2021)
Eliminación de cortes en el sistema NJ (versión del 20/03/2021)
Eliminación de cortes en la Aritmética de Heyting (HA) (versión del 26/03/2021)
Relaciones entre HA y PA (versión del 05/04/2021)
El cálculo lambda puro (versión del 23/04/2021)
El cálculo lambda simplemente tipado (versión del 30/04/2021)
La correspondencia de Curry-Howard (versión del 03/05/2021)
Sistema T de Gödel y eliminación de cortes en HA (versión del 07/05/2021)
Sistema F y eliminación de cortes en la Aritmética intuicionista de segundo orden (HA2) (versión del 24/05/2021)
La teoría de tipos de Martin-Löf (versión del 10/06/2021)
El cálculo de construcciones y sus extensiones (versión del 28/06/2021)
Equivalence between type theories and set theories (en inglés, versión del 2/07/2021)

Prácticos