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 1009 on

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