Validationexamen
EnseignantClaudia Faggian et Gabriele Vanoni
Années Master Logique Mathématique et Fondements de l'Informatique M2 Logos

Syllabus

La théorie de la démonstration a connu au moins deux évolutions majeures au cours du siècle dernier suite aux théorèmes d'incomplétude de Gödel. La première a eu lieu dans les années 30, immédiatement après les résultats d'incomplétude, avec l'introduction et l'étude de la déduction naturelle et du calcul des séquents par Gentzen et du lambda-calcul par Church. Church montrait alors l'indécidabilité du calcul des prédicats via le lambda-calcul tout en introduisant un modèle de calcul universel tandis que Gentzen déduisait la consistance de divers systèmes logiques comme corollaire de l'élimination des coupures en calcul des séquents.

La seconde étape a eu lieu dans les années 60 avec la mise en évidence progressive, par le biais de la correspondance de Curry-Howard, des liens profonds entre preuves et programmes, depuis la correspondance entre lambda-calcul simplement typé et déduction naturelle propositionnelle minimale jusqu'aux diverses extensions de cette correspondance au second ordre, à la logique classique et jusqu'à l'émergence de la notion de linéarité en théorie de la démonstration. La logique linéaire a profondément renouvelé les liens entre la sémantique formelle des langages de programmation d'un côté et la théorie de la démonstration de l'autre. L'algèbre linéaire s'impose comme troisième pôle de cette correspondance, en mettant au centre la notion de ressource du calcul.

Le cours fondamental a traité de la première étape. Ce cours sera consacré à quelques développements plus récents.

Sommaire

La première partie du cours est consacré à la sémantique dénotationnelle de la programmation fonctionnelle, la deuxième à la sémantique opérationnelle. Les deux parties se basent sur la théorie de la démonstration et sur le lambda-calcul.

Première partie:
- Introduction à l'assistant de preuve Agda, à la notation de Bruijn , et récapitulation du lambda-calcul non typé.
- Sémantique dénotationnelle du lambda-calcul non typé, formalisée.
- Validité, adéquation et complétude, formalisées.
- Equivalence contextuelle, exemples de modèles,  types intersection.
Deuxième partie:
  • Outils pour l'étude des propriétés opérationnelles: éléments de théorie de la récriture.
  • Induction et co-induction.
  • Connections avec la programmation fonctionnelle: lambda calculs en appel par nom et par valeur. Evaluations faible et paresseuse. Sémantique à petits et à grands pas. Equivalence observationnelle.
  • Raisonner sur l'équivalence de programmes: bisimulation et méthodes coinductives.
  • Logique Linéaire et réseaux de preuve.
  • Lambda-calcul probabiliste.

Bibliographie