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:
- Monday, 14 c.t. - 16 Informatik/Kriminologie - F122 Hörsaal 2
- Tuesday, 10 c.t. - 12 Informatik/Kriminologie - F122 Hörsaal 2
Exercise group:
-
Friday, 12 c.t - 14 Informatik - C215
-
Campus entry: Campus
Lectures
- October 15/16 : SF Vol 1, Preface + Basics
- October 22/23 : SF VOl 1, Induction, Lists, Poly
- October 29/30 : SF Vol 1, Tactics, Logic (until “Disjunction”)
- November 12/13 : SF Vol 1, Logic (after “Disjunction”) and IndProp (until “Inversion on Evidence”)
- November 19/20: SF Vol 1, IndProp (until end), ProofObjects
- November 26/27: SF Vol 1, IndPrinciples; CPDT Sec. 3.5, 3.7, 3.8
- December 3/4: SF Vol 1, Maps, Imp
- December 10: Canceled due to illness
- December 11: SF Vol 1, Imp (Rest), Auto (without eapply/eauto)
- December 18: SF Vol 1, ImpCEvalFun, Auto & SF Vol 2, Equiv (until “Behavioral Equivalence Is a Congruence”)
- January 7/8: SF Vol 2, Hoare
- January 14/15: SF Vol 2, Hoare2; CPDT Sec. 6.1