## 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

- 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.

- 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.

- 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.

- 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.

- 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