| CARVIEW |
This page contains information about the “Proof assistants” (PRFA) course in the second year (M2) of the Parisian Master in Research in Computer Science (MPRI) taught by Yannick Forster and Théo Winterhalter.
Note
Please register for the course here.
Overview
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 PRFA 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.
Main information
The class takes place in room 1004 on
- Mondays from 09:45 to 11:45
- Fridays from 10:45 to 11:45 (except on 14 Nov where we start at 9: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 email us if you have trouble installing anything before the first lecture.
Note
You can find information on how to install Rocq and for which editor to use on a dedicated subpage.
Please check your installation is correct by trying to run the test file we provide. The expected output of the test file can be seen here. Once again, contact us if you have any trouble.
A background in functional programming and logic is preferable, but not mandatory or necessary to pass the lecture. Experience in using Rocq or other proof assistants is not necessary. The class is designed to be interesting both for absolute newcomers and students with background using proof assistants.
Tip
We provide answers to frequently asked questions about Rocq in our FAQ.
Outline of the course
The course is divided over 8 weeks with two slots per week. For each week, we will provide optional advanced exercises. Doing them is not mandatory to pass the course, but we strongly encourage you to try them.
The schedule below is tentative.
- 19 Sept & 22 Sept. Overview of the course. Presentation of proof assistants. Getting acquainted with Rocq.
- 26 Sept & 29 Sept. Inductive types.
- 3 Oct & 6 Oct. Proof terms and meta-theory. Overview of other proof assistants.
- 10 Oct & 13 Oct. Mathematical modelling. Automation.
- 17 Oct & 20 Oct. Advanced elimination / induction.
- 24 Oct & 3 Nov. Meta-programming and tactics.
- 7 Nov (at 10:45) & 14 Nov (at 09:45). Equality.
- 17 Nov & 21 Nov. Dependent functional programming. Conclusion.
Evaluation
There will be an exam and a project.
The project
(v1.8, 10 November) is now online.
Warning
The project deadline is 13 November 2025 at 18:00.
The exam will be on 28 November at 08:45 in both rooms 1002 and 1004 (to make sure that all of you fit in).
Tip
You are allowed to bring an A4 double-sided, hand-written page to help you for the exam. Take the time to prepare it well.
Note
We give you access to the exam for last year to help you prepare for the exam.
Language
The course will be taught in English by default. You can still ask us questions or write the exam in French.
Related courses
- HOTT: Homotopy Type Theory, which requires taking this course
- PRFSYS: Foundations of proof systems
- PROGPROOFS: Proof of Programs
- FUN: Functional programming and type systems
- SEMPL: Models of programming languages: domains, categories, games
- ECOLO: Exploring Computational Models through Linear Logic
- SECURE: Proofs of security protocols
Related internships
Do not hesitate to contact us about advice around internships in the field, starting from the beginning of the course. We know a lot of people in the field so we can help you.
References
The most important resources for you are:
- Documentation of Rocq 9.0, list of tactics, list of commands.
- Rocq official website.
- Rocq Zulip chat which is the most active platform for asking questions about Rocq.
- Rocq Discourse which is a forum also containing announcements which you can register to (also by email).
Books to learn Rocq:
- B. C. Pierce, C. Casinghino, M. Gaboardi, M. Greenberg, C. Hriţcu, V. Sjöberg, B. Yorgey. Software Foundations (Volume 1).
- A. Chlipala. Certified Programming with Dependent Types.
- Y. Bertot, P. Castéran. Interactive Theorem Proving and Program Development, Rocq’Art: The Calculus of Inductive Constructions.
Other related documents:
- G. Smolka. Modeling and Proving in Computational Type Theory Using the Rocq Proof Assistant. Lecture Notes.
- C. Angiuli, D. Gratzer. Principles of Dependent Type Theory.
- The Univalent Foundations Program, Institute for Advanced Study. Homotopy Type Theory.
- E. Rijke. Introduction to homotopy type theory.
- A. Mahboubi, E. Tassi. Mathematical Components book.
- I. Sergey. Programs and Proofs: Mechanizing Mathematics with Dependent Types. Lecture Notes.
This course has been taught in different formats since 1997, by Christine Paulin-Mohring, Benjamin Werner, Bruno Barras, Hugo Herbelin, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Assia Mahboubi, Matthieu Sozeau, Yannick Forster, and Théo Winterhalter. Parts of the material we teach is taken or inspired from previous iterations of the course.