Introduction
The 2023-2024 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 may vary. 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.
As for the start of the semester, the course will take place in Sophie Germain building:
Aim of the course and organization
Goals of the course
The course has four main goals:
to serve as an introduction to (functional) programming (in Coq);
to serve as an introduction to the mechanization of proofs in Coq, and more generally to proof assistants;
to investigate the basic properties of the logical framework on which Coq is designed, the Calculus of Inductive Construction (CIC), a extension of Martin-Löf dependent type theory;
to give you enough familiarity with Coq proof assistant so that you can use it during your research internship.
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.
Weekly organization
Every week, students will have:
Regarding homework
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).
Activating your accounts in the computer labs
In order to log in the computers:
the login to be used is not directly your university credentials (@u-paris.fr), you need to use your UPC student account to activate your access to the computer labs,
-
in case of trouble, the guest account allows you to use the computer anyway: bring a usb key in that case so that you can store the files you work on.
Course material
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.
TP0: First steps… Open the webpage for TP0, download the file TP0.v and follow the instructions!
Lecture 1: Introduction to functional programming in Coq (types and terms; the pure and simply typed lambda-calculus and the arrow type; first steps into CIC, the type theory of Coq: the sorts Type, Set and Prop & dependent product; global and local definitions; sections; global and local declarations; recursive functions definitions; introduction to inductive types.)
Lecture 2: Introducing inductive types
Lecture 3: Advanced inductive types and introducing dependent types
Lecture 4: Advances dependent types
Lecture 5: More dependent types and ointroducing the proof environment ((o) dependent sum, (i) proofs as programs, (ii) encounter with the third kind: Prop and specific dependent formation rules of CC (iii) Coq proof environment and elementary tactics)
Lecture 6
Lecture 7
Lecture 8
Lecture 9
Lecture 10
Lecture 11
Lecture 12
Bibliography
-
-
-
-
Coq'Art, by Yvers Bertot and Pierre Castéran (resources available in french and english)
-