NewsCurrently, 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.
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
- Mtac 2
The first lecture is on TBA, the last lecture on TBA.
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.
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.