Parisian Master of Research in Computer Science

Master Parisien de Recherche en Informatique (MPRI)

Fondements des systemes de preuves (24h, 3 ECTS)

Responsable : Gilles Dowek

Langue / Language

The course will be in english if needed.

Plan du cours et intervenants prévus pour 2010-2011

1. Benjamin Werner (14h)
2. Assia Mahboubi et/ou Sylvie Boldo (10h)

Objectifs

Ce cours étudie la notion de preuve en tant qu'objet mathématique et informatique. Il présente plusieurs théories logiques en mettant l'accent sur les théories des types d'ordre supérieur. Il s'intéresse plus particulièrement à l'articulation entre les notions de raisonnement et de calcul.

Ce cours est un prérequis au cours Assistants de preuve : principes et application à la preuve de programmes qui développera les applications de ces formalismes aux assistants de preuves, en particulier le système Coq en vue de modéliser et de certifier des programmes ainsi que de mécaniser des théories mathématiques.

Plan du cours

1. Déduction modulo
2. La théorie des ensembles, la théorie des types simples.
3. Expression et existence de fonctions en théorie des types : fonctions exprimables sur les entiers de Peano, les entiers de Church; opérateur de choix et de description; représentation de fonctions en logiques intuitionniste ou classique.
4. Logique intuitionniste, isomorphisme de Curry-de Bruijn-Howard, types dépendants.
5. Types inductifs : système T de Gödel et théorie des types de Martin-Löf.
6. Polymorphisme : système F, Normalisation, élimination des coupures, représentation des fonctions.
7. Calcul des Constructions, généralisation aux systèmes de types purs. Représentation des fonctions.
8. Calcul des Constructions Algébriques

Pré-requis

Programmation

un langage fonctionnel (Ocaml)

Langages

typage (systèmes de types élémentaires, inférence de type à la ML)

Logique

calcul propositionnel, logique du premier ordre, systèmes de preuves en déduction naturelle

Calculabilité

lambda-calcul pur (syntaxe, alpha-conversion, béta-réduction, confluence, normalisation)

Mathématique

ordres bien fondés

Réécriture

Notions de base de réécriture du premier ordre

Bibliographie

• B. Nordström, K. Petersson, J. Smith. Programming in Martin-Löf's Type Theory.
• The Coq Proof Assistant V7 http://coq.inria.fr/doc-fra.html.
• G. Dowek. Théorie des Types

Les années précédentes

• Année 2009-2010
• Année 2008-2009
• Année 2007-2008
• Année 2006-2007

Équipe pédagogique

Examens des années précédentes

• 2007-2008