This page contains information about the “Proof assistants” (PRFA, 2-7-2) 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.

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 Coq, with the objectives to have the students

- to be able to use Coq in other courses,
- use Coq in an internship,
- learn other proof assistants or become an expert user of Coq 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 Coq 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* from 08:45 to 11:45. The first lecture is on
*September 23rd*.

Students must bring their own laptop with Coq installed *prior to the first
lecture* (⚠️): we require version 8.18 together with Equations and
MetaCoq installed. To that end, we assume students have installed
the corresponding Coq Platform. Please don’t hesitate to send us an
email
if you have trouble installing anything before the first lecture.

Note

You can find information on how to install Coq 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. 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 Coq is not necessary. The class is designed to be interesting both for absolute newcomers and students with background using Coq.

Tip

We provide answers to frequently asked questions about Coq in our FAQ.

The course is divided over 8 weeks with the tentative following schedule. For each lecture, we plan to provide optional advanced exercises. Doing them is not mandatory to pass the course, but we encourage you to try them.

- 23 Sept. Overview of the course. Presentation of proof assistants. Getting acquainted with Coq. Live coding
- 30 Sept. Inductive types.
- 7 Oct. Proof terms and meta-theory. Overview of other proof assistants.
- 14 Oct. Equality.
- 21 Oct. Mathematical modelling. Automation.
- 28 Oct. Meta-programming and tactics.
- 4 Nov. Advanced elimination / induction.
- 18 Nov. Dependent functional programming. Conclusion.

There will be an exam and a project, each counting for half of the final grade.

The course will be taught in English by default. You can still ask us questions or write the exam in French.

- Foundations of proof systems
- Proof of Programs
- Functional programming and type systems
- Models of programming languages: domains, categories, games

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.

The most important resources for you are:

- Documentation of Coq 8.18.0, list of tactics, list of commands.
- Coq official website.
- Coq Platform 8.18.0 release.
- Coq Zulip chat which is the most active platform for asking questions about Coq. A (not so easy to read) archive is publicly available.
- Equations website.
- MetaCoq website.
- VSCoq Legacy for VSCode.
- VSCoq Legacy for VSCodium.
- VSCoq2 for VSCode.
- VSCoq2 for VSCodium.

Books to learn Coq:

- 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, Coq’Art: The Calculus of Inductive Constructions.

Other related documents:

- 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.
- G. Smolka. Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant. 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.