Table of Contents
Fondements des systemes de preuves / Foundations of proof systems (24h, 3 ECTS)Responsable : Gilles Dowek LanguageThe course is in English (unless clearly only french speakers present) Teaching in 2023  2024Main Page of the CourseObjectivesThis course is about the notion of formal proof in mathematics and in informatics. It presents several logical formalisms, including type theories, focusing on the fact that they are meant to be used in proof systems such as Coq, Agda, HOL, Isabelle, PVS. We will treat in depth the articulation between reasoning and computation. This course is a prerequisite / is linked to to the course Proof Assistants (272) It is good to attend to both courses, although you are not required to. We may to some lightweight exercises in Coq towards the end of the lessons in 271. Not so much to learn Coq, but in order to view the material in a different way. So it is a good idea to bring your computer with Coq installed (again see the instructions on the page of 272) When and where ?The lectures are on Mondays starting Sept. 18th, from 16:1519:15, in the Sophie Germain Building, room 1004. ScheduleThis is tentative
ExamWritten exam. Date TBA PrerequisitesSome familiarity with:
InternshipsBibliographyPast examsTeam
