The 2024-2025 PF2 course is taught by Alexis Saurin. It was previously taught by Pierre Letouzey and an important part of the course material is adapted / expanded from his previous material and by (older) material from Alexandre Miquel.
The rooms for the class and lab sessions is 2006. Look at the schedule of LMFI to get the proper information and in case of doubt, check the course discord on which I will post changes in classroom assignment.
The course has four main goals:
The course will start with a first period focusing on programming using Coq, for approximately 4 or 5 weeks. Then, we will shift to using Coq as a proof assistant. Globally, I plan that 5 weeks are dedicated to programming with Coq (TP0 non included) and 7 weeks are dedicated to proving with Coq.
I consider that you should spend “about” the same amount of time studying in class than outside class. More precisely, for PF2, students are expected to spend 3H to 5H a week of extra working time (studying course material, doing some of the additional exercise of the TP, doing some additional reading given in class or completing some proof / example that has been only partially treated in class.
This is of course purely indicative: some of the student will need less, some might need more and you may decide focusing some week more on this class and some other week more on another class. The thing to keep in mind is that if for two consecutive weeks you provide no additional work in this course, there are good chances that you end up being lost.
The course exam will consist in a formalization project to be handed early in the second semester (details to come around Halloween / Toussaint).
In order to log in the computers:
The Coq files corresponding to the course as well as addition material will be gathered on this git repository from which you can download them.