Programming Languages

Interactive Theorem Proving

This course is an introduction to interactive theorem proving and advanced functional programming, mostly using the Coq proof assistant.

This course is for students interested in:

  • The foundational theories of mathematics, most notably type theory and logic
  • Practical interactive theorem proving in a state-of-the-art proof assistant
  • Advanced functional programming languages and their relation to constructive mathematics via the “Curry-Howard Isomorphism”
  • Program verification and “certified programming”
  • Programming Language Semantics

The course can be found on Alma



The lecture will take place on the following dates:

  • Tuesday, 14 c.t. - 18 in room F122 on the Sand

The tutorials will take place on the following dates (beginning on April 24th):

  • Monday, 16 c.t. in room F122 on the Sand.

Lecture Resources

We covered the following material during the lectures:

  • SF Vol 1: Basics, Induction, Lists, Poly, Tactics, Logic, IndProp, Maps, ProofObjects, IndPrinciples, Rel, Imp, Auto
  • SF Vol 2: Equiv, Hoare, Hoare2
  • CPDT: 3,5, 3.7, 3.8, 6.1, 6.2, 8.1, 8.3.

Final Exam

The final exam will take place on 24.07.2023 at 16 c.t. in room F119 on the Sand


  • The Coq Proof Assistant Link
  • The Software Foundations Series Link
  • Adam Chlipala, Certified Programming with Dependent Types CPDT