Thorsten Altenkirch
School of Computer Science and IT
University of Nottingham
The aim of this course is to give an overview over the concepts of Intuitionistic Type Theory which is based on the ideas of Per Martin-Löf. We shall use Randy Pollack's LEGO system to play with Type Theory.
In intuitionistic logic existential witnesses can be effectively computed from proofs, but this is an external procedure - you cannot reason about proofs or witnesses. This shortcoming is remedied by Type Theory where a proposition is identified with the set of its proofs. Thus Type Theory is at the same time a logic and a programming language with a quite sophisticated type system.
The course includes an overview of intuitionistic logic and its constructive semantics (proposed by Brouwer, Heyting and Kolmogorov). We shall then introduce the basic constructions of Type Theory: Pi-types, Sigma-Types, identity types, inductive definitions (including inductively defined familes) and universes. As a non-trivial example we shall formalize completeness and normalisation for minimal intuitionistic propositional logic. Final we will discuss the meta theory of Type Theory.