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

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

Ressources

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