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
Dozenten
Schedule
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