Preuves et programmes : Outils classiques
8 ECTS, semestre 2, 12 semaines
| Validation | examen |
| Enseignant | Antonio Bucciarelli et Claudia Faggian |
| Horaires hebdomadaires | 4 h CM |
| 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:
- Interprétation des preuves et des programmes : interprétations du lambda-calcul simplement typé et de PCF dans une catégorie cartésienne fermée (exemples de CCC, théorème d'adéquation).
- Exemples de modèles (domaines de Scott, espaces de cohérence, modèles de jeux).
- Problèmes de définissabilité et d'adéquation complète.
- Relations logiques.
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
- R. AMADIO : Operational methods in semantics (available on HAL https://hal.archives-ouvertes.fr/cel-01422101v1).
- R. AMADIO, P.-L. CURIEN : Domains and lambda-calculi (Cambridge Tracts in Theoretical Computer Science 46, Cambridge University Press, 1998).
- D. SANGIORGI: Introduction to Bisimulation and Coinduction (Cambridge University Press, 2011)