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



Lecture: The lecture will take place online via Zoom on the following dates:

  • Tuesday, 10 c.t.
  • Thursday, 10 c.t.

The Zoom room for this lecture is available here: zoom lecture

Exercise group: The exercises will take place online via Zoom on Friday, 12 c.t. The Zoom room for this exercise group is available here: zoom exercises

If you intend to participate in this lecture, please register in the forum and follow the instructions in the “about” post of the ITP category.




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