
COPLASCopenhagen Programming Language Seminar 
We give an overview over what is known about the proof theory of MartinL{\"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 (Wtypes) and universes. Then we give a brief introduction into a generic type theory, the theory of inductiverecursive 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
proglangrequest@mail.itc.dk with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see
http://www.coplas.org