Saarland University Computer Science

Advanced Coq Programming Prof. Gert Smolka, Yannick Forster, Fabian Kunze

Advanced Course, 6 credit points, Summer Semester 2020

Registration for this course is open until Friday, 20.03.2020 23:59.


Currently, no news are available

Advanced Coq Programming

All information on this website is preliminary and subject to change.

This advanced course is a practical, "hands-on" course on the Coq proof assistant.

First phase

The first part is a block course, with lectures in the morning and tutorials or office hours in the afternoon. Attendance in lectures is expected.

We plan to cover (a subset of) the following topics in the lectures:

  • Advanced automation: Tactics, Hints and Ltac
  • Type classes, canonical structures
  • Setoid rewriting
  • ssreflect and mathcomp
  • Coinduction and coinductive definitions
  • Implementation of Coq
  • Useful Coq plugins, projects, and libraries
    • Autosubst
    • Equations
    • Iris
    • MetaCoq
    • Mtac 2
    • Paco
    • ...

The first lecture is on TBA, the last lecture on TBA.

Second Phase

The second part of the course is a project phase of 5 weeks, lasting until TBA. Students work on their own on an interesting mechanisation topic with an advisor. We have a list of interesting topics, but are open to suggestions. Credit and grades will be based on the project. We do not expect a mathematical writeup. However, a well-documented and well-readable formalisation may improve the grade.


In the TBA, students will give a short, 5-10 minute presentation on their project. The presentation should give an overview of the mechanisation and point out the most interesting details.

Participation Requirements

We require familiarity with the proof assistant Coq. Students who have not taken a Coq-related lecture (Introduction to Computational Logic, Semantics, Computational Logic 2 or a similar course at another university) may have to prove their familiarity in order to participate.