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
Dozenten
Schedule
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.
- Alma entry: Alma