Over all 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.
Time and place:
The lectures will be held on Mondays from 10:15 to 12:00 and Thursdays from 15:15 to 17:00, starting 4 November, in room 306, house 6, Kräftriket (Roslagsvägen 101).
P. Martin-Löf, Intuitionistic type theory. Notes by Giovanni Sambin of a series of lectures given in Padua 1980. Bibliopolis 1984. Out of Print. Electronic version available here.
E. Palmgren. Lecture notes on type theory, 2014. PDF.
Articles about lambda-calculus and models of type theory: Distributed during the course.
H.P. Barendregt. Lambda-calculus with types. In: (S.\ Abramsky and T.S.E. Maibaum eds.) Handbook of Logic in Computer Science vol. 2, Oxford University Press 1992. PDF
Homotopy Type Theory: An Introduction to Univalent Foundations, Institute of Advanced Study 2013. Open access E-book available here.
P. Martin-Löf. On the Meanings of the Logical Constants and the Justifications of the Logical Laws. Nordic Journal of Philosophical Logic, 1(1): 11–60, 1996. PDF.
B. Nordström, K. Peterson and J.M. Smith. Programming in Martin-Löf's Type Theory: An Introduction. Oxford University Press, Oxford 1990. Out of Print. Open access E-book available here.
A. Ranta. Type Theoretical Grammar, Oxford University Press, Oxford, 1994.
The Coq proof assistant, documentation and tutorials can be found here.
Examination and Grading
The examination will consist in four hand-in problems, and an oral examination. If you wish to take the course as a PhD-course, an extra project or seminar will be required.
|Problem set||Date of issue and hand-in||Maximum score|
|1||14 Nov. - 28 Nov.||20|
|2||28 Nov. - 12 Dec.||20|
|3||5 Dec. - 20 Dec.||30|
|4||12 Dec - 9 Jan.||30|
|A||90-100 points + oral exam|
|B||80-100 points + oral exam|