Type Theory
Starting November 4 a course on type theory starts which should be suitable for advanced students, PhD-students and researchers.
Tid: Må 2013-11-04 kl 10.15 - 12.00
Plats: Room 306, building 6, Kräftriket, Department of mathematics, Stockholm university
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.