Saarland University Computer Science

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

Advanced Course, 6 credit points, Summer Semester 2020

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. The course takes place at Saarland University, but for students unable to attend physically we also offer full remote participation via Zoom.

First phase

The first part is a block course, with lectures, exercise sessions, office hours, and guest lectures by international researchers. Attendance in lectures is expected.

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

  • Advanced automation: Tactics, Hints and Ltac
  • Dependent, nested, and mutual inductive types
  • Type classes
  • Setoid rewriting
  • ssreflect
  • Foundations and Implementation of Coq
  • Useful Coq plugins, projects, and libraries
    • Autosubst
    • CertiCoq
    • Coq-Elpi
    • Equations
    • Extraction
    • Iris
    • MetaCoq (and TemplateCoq)
    • the Program Package
    • QuickChick
    • the Verified Software Toolchain (VST)

The first lecture is on October 12th at 10:00 am in HS 003, building E1 3 or via Zoom, the last lecture on October 23rd.

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, only well-documented code.


On 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.