Type theory (advanced level, 7.5 hp)

Course code and home page

Stockholm University course code: MM8036

Overall motivation and description

Modern type theory is a logical theory that has dual roles as a foundational system for mathematics, on the one hand, and as a (theoretical) programming language, on the other. Type theory is widely used in computer science in formal verification of systems and programs, and also for constructing large scale formal proofs in mathematics. The theory is ideally suited as a foundation for constructive mathematics, and in fact, proving a theorem in theory is the same thing as constructing a program that computes what the theorem says exists. This can been seen in semi-automated proof support systems as Coq and Agda which will be used during the course. Type theory is also the background for the novel developments in homotopy theory and univalent foundations by Voevodsky and his group.

The course deals to a large extent with theoretical questions regarding type theory. Thus it will start with fundamental notions such as simple types, lambda-calculus, reduction rules, confluence and normalization, and then go on to more advanced theories with dependent types (Martin-Löf type theory) and the notions particular to that, such as contexts, judgments forms, inductive types, type universes, and their semantics, both informal and formal.

Aim of the course

The student should be able to define the basic notions and derive the first properties in lambda calculus and type theory, and should be able to explain and prove fundamental theorems about type theory and its semantics. Another important skill to be acquired is how to use type theory to formalize and prove theorems in mathematics, and with the help of that extract algorithmic content from proofs.

Erik Palmgren, July 5, 2013