Proof assistants have a wide range of applications from mathematical theorems (including some, like the four colour theorem, that have no proof without the use of a computer) to program verification (which can be crucial for critical software, e.g. in aviation settings or cryptography).

The course aims at bringing students to a point where they are familiar enough with one proof assistant, namely Rocq, with the objectives to have the students

• to be able to use Rocq in other courses,
• use Rocq in an internship,
• learn other proof assistants or become an expert user of Rocq via self study,
• ultimately use or study proof assistants as part of a PhD.

To this end, the course focuses on introducing general concepts found in proof assistants through practice in the Rocq proof assistant, and also mentions aspects of the underlying type theory. A complementary introduction to type systems is part of the course Foundations of proof systems.

The class takes place in room 1004 on

• Mondays from 09:45 to 11:45
• Fridays from 10:45 to 11:45

The first lecture is on September 19.

Students must bring their own laptop with Rocq installed prior to the first lecture (⚠️): we require version 9.0 together with Equations and MetaRocq installed. Please don't hesitate to send us an email if you have trouble installing anything before the first lecture.

A background in functional programming and logic is preferable, but not mandatory or necessary to pass the lecture. Experience in using Rocq is not necessary. The class is designed to be interesting both for absolute newcomers and students with background using Rocq.