Copenhagen Programming Language Seminar

Proof theory and Martin-L{\"o}f Type Theory

Anton Setzer
Swansea University

Tuesday, May 27, 2008, 13:00-14:00
ITU, Rued Langgaards Vej 7, 2300 Copenhagen S. Auditorium 2


We give an overview over what is known about the proof theory of Martin-L{\"o}f Type Theory (MLTT). We start by giving a basic introduction into ordinal theoretic proof theory. This will justify a type theoretic program, namely the development of proof theoretically strong extensions of MLTT. This will amount as well to the development of new data types, some of which have been used already in programming.

We investigate the basic principles used for analysing various constructs of MLTT, namely tree types (W-types) and universes. Then we give a brief introduction into a generic type theory, the theory of inductive-recursive definitions, which subsumes most standard extensions of MLTT, and which has been used in the area of generic programming. Finally we look at two constructs which add substantial strength to MLTT, namely the Mahlo universe and the $\Pi_3$-reflecting universe.

Scientific host: Carsten Schürmann. Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org