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
- April 18: SF Vol 1, Basics + Induction
- April 25: SF Vol 1, Lists + Poly
Final Exam
The final exam will take place on 24.07.2023 at 16 c.t. in room F119 on the Sand