Advanced type systems offer a compelling way for proving absence of entire classes of errors without even running any program. We will cover among other things the following topics:
- implementing type systems
- programming with dependent types
- the lambda calculus, simple types, polymorphism, and more
- typing rules, type checking, type inference, type soundness, and more
- syntax, semantics, and mechanization of type systems properties
The course will feature homework using the dependently-typed Lean4, a modern functional and dependently typed programming language, that can be used both to write efficient programs, but at the same time serves as an interactive proof assistant, exploiting the proofs-as-programs correspondence (also known as Curry-Howard).
This is a new course. Before scaling up to at-will registration, participation is limited this semester. Applications will be made on the first lecture day, and selected participants will be notified by/on the second lecture day.
- Dozent*in: David Richter
Erste Veranstaltung: Thursday, 16 April 2026, 13:30