Type Systems for Computer Assisted Proofs

Dr. Alexandre Miquel

       
       
       
       
       
       
       
       

@ El curso será en inglés y se recomienda especialmente para alumnos de grado y posgrado que hayan cursado Reescritura y Calculo Lambda y Sustituciones Explícitas

@ Correlativa: es recomendable tener algun conocimiento de lógica

@ Duración: 3 semanas, del 29 al 17 de diciembre.

@ Total de horas: 12

@ Puntaje: 1, para la carrera de grado y 1/2 punto para posgrado

(sujeto a ser aprobado por las comisiones correspondientes)

Los interesados por favor contactarse con el Dr. Alejandro Ríos

       

Contenido:

System F:

Programming in system F (data types, etc.)

Church-style & Curry-style presentation,

Strong normalisation

Proof-extraction in 2nd order arithmetic (HA2)

- Natural deduction, HA2/PA2 - The Curry-Howard correspondence

- Program extraction from HA2 to system F

Systems with dependent types

- Martin-Löf type theories

- Calculus of Inductive Constructions

Introduction to the Coq proof assistant

Extracting programs from proofs in Zermelo & Zermelo-Fraenkel set theories

 

       
Bibliografía y sitios de interes