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 2021 - 2022

Objectives

The topic of this course are the notions of formal proofs and of logical formalisms. The latter are considered through their possible implementation and use in proof systems (much as a programming language is implemented by a compiler).

We present several formalisms, including type theories used in several proof systems such as Coq, Agda, HOL, Isabelle, PVS. A particular point of attention will be the articulation between reasoning and computation.

When and where ?

The lectures are on Tuesdays from 16:15 to 19:30, in the Sophie Germain Building, room 1002. First course Sept. 14th

Schedule

Sept 14th : Motivations, aim (good formalisms), First-Order Logic & Natural deduction, Deduction Modulo, Logical Cuts.

slides (lecture 1)

Exam

Final Exam, length 2 hours. Date TBA

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