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 2022 - 2023ObjectivesThis 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. This course is a prerequisite to the course Assistants de preuve : principes et application à la preuve de programmes. When and where ?The lectures are on Mondays from 12:45 to 16:00, in the Sophie Germain Building, room 1004. ScheduleSeptember 19th: Natural deduction - The notion of theory September 26th: The notion of model - Exercises October 3rd: Arithmetic - Naive set theory October 10th: Simple type theory - Exercises October 17th: The termination of proof reduction October 24th: Dependent types - Exercises November 7th: Inductive types - Polymorphism November 14th: Master class: Théo Winterhalter - Preparation of the exam ExamNovember 28th, 13:00-14:30. Prerequisites
Internships
Frédéric Blanqui: Inter-system translation of recursive functions
Bibliography
Lecture notes
Past examsTeam
|