Advanced type systems offer a compelling way for proving the absence of entire classes of errors without even running any program. We will cover, among other things, the following topics:
- programming with advanced type systems
- lambda calculus, simple types, polymorphism, dependent types
- typing rules, type checking, type inference, type soundness
- implementing type systems for programming languages
Participation is limited. Applications will be made on the first lecture date, and the selection will be announced on the second lecture date.
Recommended Prerequisites:
- Lecture “Functional and Object-Oriented Programming” (FOP)
- Lecture “Concepts of Programming Languages” (COPL)
Notes
- The course will include practical homework examples in the functional, dependently-typed programming language and proof assistant Lean 4, which can be conveniently installed as a plugin for VSCodium / VSCode.
Turnus: Summer
Kind: IV 06cp
In Tucan: 20-00-1246-iv Type Systems