Courses

Formal Foundations of Programming Languages

Our course for the Master's Program, "Formal Foundations of Programming Languages", is offered every fall. It covers the theory of type systems from the Simply-Typed Lambda Calculus via System F to mutable state, recursive types, and linear types. We discuss traditional type safety proofs via progress and preservation, logical relations, and how to reason about "unsafe code"—terms that are not well-typed but uphold the invariants of the type system in a non-trivial way, and hence can be safely composed with arbitrary well-typed code. The proofs are carried out in the board and in Rocq.

The lecture notes for this course are publicly Download available for download here (PDF, 739 KB).