Table of Contents
Fondements des systemes de preuves / Foundations of proof systems (24h, 3 ECTS)Responsable : Gilles Dowek LanguageThe course is in English. Teaching in 20202021ObjectivesThis course focuses on the notion of formal proof in mathematics and in informatics. It presents several logical theories, including type theories used in several proof systems such as Coq, Agda, HOL, Isabelle, PVS. In particular we will treat in depth the articulation between reasoning and computation. When and where ?The lectures are on Wednesdays from 16:15 to 19:30, in the Sophie Germain Building, room 1013. Schedule
ExamWednesday, December 2nd, 16h1518h15, room 1013. Course notes and personal documents allowed. Prerequisites
Internships
Bibliography
Course notes: Proofs in theories Slides: Lecture 1, Lecture 2, Lecture 3, Lecture 4, Lecture 5, Lecture 6, Lecture 7, Lecture 8, Lecture 9, Lecture 10, Lecture 11. Exercises: Exercises 1, Exercises 2, Exercises 3. Past exams
Team
