Précédent Remonter

Preuves et types

Cours de recherche (24h de cours, travail sur des articles scientifiques)

Cours : Tom Hirschowitz (Tom.Hirschowitz)



Présentation générale
Le cours porte sur le développement de l'isomorphisme de Curry-Howard entre preuves/formules et programmes/types.

Après les théorèmes d'incomplétude de Gödel, on a commencé à étudier la logique comme un phénomène physique, qu'on essaie de modéliser relativement à certaines propriétés observables. Les modèles de la logique comprennent généralement des notions de formule, de preuve et d'absurdité. Ils permettent de représenter fidèlement des parties significatives des mathématiques et exhibent de bonne propriétés en liaison avec la démonstration automatique, telles que l'élimination des coupures, la propriété de disjonction, ou la propriété d'existence. Plus important encore, bien que moins objectivement, ils mettent en évidence les symétries intuitives entre « et » et « ou » et entre les quantificateurs existentiel et universel.

Un courant particulièrement productif de modèles de la logique consiste à voir les preuves comme des programmes et les formules comme des types. Par exemple, une preuve de « A et B implique B » est un programme de type « A × B → B », qui attend une paire en argument et renvoie la seconde composante de cette paire. La propriété fondamentale de ces modèles est que l'exécution des programmes correspond à l'élimination des coupures dans les preuves, c'est-à-dire en gros la réduction de preuves en des preuves déductibles automatiquement. Cette correspondance est appelé l'isomorphisme de Curry-Howard.

Le cours va couvrir des instances de plus en plus sophistiquées de l'isomorphisme de Curry-Howard: la logique intuitionniste minimale, la logique intuitionniste du second ordre et la logique linéaire classique multiplicative exponentielle.

Plan indicatif
  1. Rappels de logique
    1. Déduction à la Hilbert
    2. Déduction naturelle
    3. Calcul des séquents
  2. Interprétation fonctionnelle des preuves en déduction naturelle intuitionniste
    1. Déduction naturelle intuitionniste minimale et λ-calcul simplement typé
    2. Déduction naturelle intuitionniste du second-ordre et système F
    3. Introduction à la réalisabilité
  3. Logique linéaire
    1. Calcul des séquents linéaire classique
    2. Traductions des logiques classiques et intuitionnistes standard
    3. Réseaux de preuves
    4. Un modèle concurrent
  4. Approfondissements (s'il reste du temps)
    1. Calcul des séquents classique et calcul dual
    2. Caractérisation de la classe de complexité PTIME
Bibliographie
Précédent Remonter