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 2018-2019

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 each Wednesday from 8:45 to 12:00, in the Sophie Germain Building, room 1004

Schedule

September 12th: Natural deduction - The notion of theory
September 19th: The notion of model - Exercises
September 26th: Arithmetic - Naive set theory
October 3rd: Simple type theory - Exercises
October 10th: The termination of proof reduction
October 17th: Dependent types - Exercises
October 31st: Inductive types - Polymorphism
November 14th: Master class - Preparation of the exam

No lectures on October 24th and November 7th

Exam

November 21st, 9h-10h30, Sophie Germain Building, room 1003

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

Bibliography

Internships

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