Lectures series: Introduction to Intuitionistic Type Theory

Important Remark

In order to reduce email traffic, in future the lectures will no longer be announced as previously on the email lists. If you want to get informations via email, please send an email to Anton Setzer , Replace '_dot_' by '.' and '_at_' by '@' in 'a_dot_g_dot_setzer_at_swan_dot_ac_dot_uk' Thank you.


The main time will be on Wednesday 15 - 17, but in accordance with obligations of the audience and of the lecturer this time will be changed on a time to time basis.

Continuation of Lecture Postponed

The continuation of this series will be postponed till at least November, maybe even till January. However, the course on Constructive Logic and Lambda Calculus, given by myself, covers topics which are closely related to this course and is therefore recommended.


Anton Setzer, originally Department of Mathematics, Uppsala University, now Department of Computer Science, University of Wales Swansea.


Per Marin-Löf's type theory is a constructive frame-work for carrying out mathematical proofs. Originally defined for carrying out constructive mathematics, it has been of growing interest in computer science, since in it proofs and programs are the same. Proofs are carried out by defining a program which computes an element of the proposition to be proved. Therefore it provides a potential framework for the development of programs together with their correctness proofs.

We will give a introduction to this theory starting from a very elementary level. Because of the background of the lecturer, a more proof theoretic perspective will be taken. Recent extensions like the Mahlo universe and the general theory of inductive recursive definitions will be covered in later lectures. The relevance of it for the foundations with mathematics will be discussed.