Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Fondements des systemes de preuves / Foundations of proof systems (24h, 3 ECTS)

Responsable : Gilles Dowek

Language

The course is in English.

Teaching in 2022 - 2023

Objectives

This 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.

Schedule

September 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

Exam

November 28th, 13:00-14:30.

Prerequisites

The notion of inductive definition.
The notions of free and bound variables, alphabetic equivalence, and substitution.
The syntax of (many-sorted) predicate logic.
The natural deduction.
The untyped lambda-calculus.
The simply typed lambda-calculus.
The expression of computable functions in arithmetic, in the language of rewrite rules and in the lambda-calculus.

Internships

Bibliography

Past exams

Team

Gilles Dowek DR INRIA and ENS Paris-Saclay
Benjamin Werner PR Ecole polytechnique
Pierre-Yves Strub MdC Ecole polytechnique

 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA