This course is an introduction to interactive theorem proving and advanced functional programming, mostly using the Rocq 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

• Klaus Ostermann
  ProfessorKlaus Ostermann
• Filip Šimić (Office: Room B211)

Forum

Participants should register in the forum ps-forum.cs.uni-tuebingen.de and send a message to user filip in order to be admitted to the subforum.

Schedule

The lecture will take place on the following dates:

• Tuesday, 14 c.t. - 16 in room F122 on the Sand
• Thursday, 12 c.t. - 14 in room A104 on the Sand

The tutorials will take place on the following dates:

• Thursday, 14 c.t. - 16 in room F122 on the Sand.

Resources

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