Preuves et programmes : Outils classiques

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é aux développements depuis les années 60 et présentera les outils classiques pour l'étude de la correspondance de Curry-Howard. Après quelques rappels et compléments du cours fondamental, le cours se concentrera sur deux concepts fondamentaux, le second-ordre et la linéarité, et à leurs développements, notamment dans un cadre algébrique. On appliquera notamment les résultats du cours à l'étude de PCF, un langage de programmation idéalisé.

Sommaire

• Introduction et compléments (rappels sur le lambda-calcul et la théorie de la démonstration).
• Trois exemples de calculs : lambda simplement typé, Système F (Logique et arithmétique du second- ordre, théorème de normalisation forte) et PCF.
• Logique linéaire : décomposition linéaire, calcul des séquents linéaire, réseaux de preuves et correction, élimination des coupures, traductions linéaires du lambda-calcul.
• 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), sémantique catégorique de LL et exemples de modèles (domaines de Scott, sémantique relationnelle, modèles vectoriels), interprétations interactives, théorèmes d’adéquation.
• Extensions de Curry-Howard : Curry-Howard pour la logique classique, extensions et variantes de la logique linéaire (logiques allégées, logiques différentielles, logiques avec points fixes, ...), PCF probabiliste (espaces cohérents probabilistes et complète adéquation pour PCF probabiliste)

Bibliographie

• R. AMADIO, P.-L. CURIEN : Domains and lambda-calculi (Cambridge Tracts in Theoretical Computer Science 46, Cambridge University Press, 1998).
• P.-L. CURIEN, H. HERBELIN, J.-L. KRIVINE, P.-A. MELLIES : Interactive Models of Computation and Program Behavior (Panorama et Synthèses, Société mathématique de France, 2009).
• R. DAVID, K. NOUR, C. RAFFALLI : Introduction à la logique Théorie de la démonstration (Sciences Sup, Dunod, 2004).
• J.-Y. GIRARD, Y. LAFONT, P. TAYLOR : Proofs and Types (Cambridge University Press, 1989, disponible sur la page de P. Taylor).
• R. HARPER : Practical Foundations for Programming languages (Camb Univ Press, 2012)
• J.-L. KRIVINE : Lambda-calcul : Types et Modèles (Masson, 1990, ou E. HORWOOD : Lambda-calculus : types and models version augmentée, en anglais, 1992).
• B.C. PIERCE : Types and Programming Languages (MIT Press, 2002).

• inscriptions
• calendrier
• accès
• Questions fréquentes