Type Theory in Rosario

Intensive Course

This is the material related to a one week intensive course starting 24 July 2011 on Type Theory at Facultad de Cs. Exactas, Ingenieria y Agrimensura Universidad Nacional de Rosario

Agda

You need to download Agda and install emacs because Agda is used via emacs.

Lecture material

1. Lecture (Monday, 25/7) : Introduction
   
   • Slides
   • Wikipedia: Zermelo-Fraenkel set theory, Intuitionistic type theory, Per Martin-Löf
   • How to type in Unicode characters for Agda in emacs.
   • Commands in Agda-mode in emacs
   • Agda file from Monday (Lunes.agda) download and load into emacs
   • Completed agda script as an html file.
2. Lecture (Tuesday, 26/7) : Propositions as sets
   
   • Agda file from Tuesday (Martes.agda) download and load into emacs
   • Wikipedia: Curry-Howard correspondence
   • Wikipedia: Excluded Middle, Proof by contradiction
   • Completed agda script as an html file.
3. Lecture (Wednesday, 27/7) : Mixing computation and resoning
   
   • Agda file from Wednesday (Miercoles.agda) download and load into emacs
   • Completed agda script as an html file.
4. Lecture (Thursday, 28/7) : Inductively defined relations
   
   • Agda file from Thursday (Jueves.agda) download and load into emacs
   • Completed agda script as an html file.
5. Lecture (Friday, 28/7) : Typed evaluation and compilation
   
   • Agda file from Thursday (Viernes.agda) (alternative version w.o. record constructors : (Viernes-alt.agda) download and load into emacs