Proofs and programs: classical tools

Syllabus

Proof theory has undergone at least two major developments over the past century as a result of Gödel's incompleteness theorems. The first took place in the 1930s, immediately after the results on incompleteness, with the introduction and study of natural deduction and sequent calculus s by Gentzen and lambda-calculus by Church. Church then showed the undecidability of predicate calculus via lambda-calculus while introducing a universal computation model while Gentzen deduced the consistency of various logical systems as a corollary of cut elimination of breaks in sequent calculus.

The second stage took place in the 1960s with the gradual highlighting, through the Curry-Howard correspondence, of the profound links between proofs and programmes, from the correspondence between simply typed lambda-calculus and minimal propositional natural deduction to the various extensions of this correspondence to the second order, to classical logic and to the emergence of the notion of linearity in proof theory. Linear logic has profoundly renewed the links between the formal semantics of programming languages on one hand and proof theory on the other. Linear algebra is the third pole of this correspondence, focusing on the notion of computational resource.

The basic course covered the first step. This course will be devoted to the developments since the 1960s and will present the classical tools for the study of the Curry-Howard correspondence. After some review and additions to the basic course, the course will focus on two fundamental concepts, the second order and linearity, and their development, particularly in an algebraic context. In particular, the results of the course will be applied to the study of PCF, an idealized programming language.

Contents

• Introduction and additions (review of lambda-calculus and proof theory).
• Three examples of calculi: lambda simply typed, System F (Logic and arithmetic of the second order, strong normalisation theorem) and PCF.
• Linear logic: linear decomposition, linear sequent calculis, proof networks and correctness, cut elimination, linear translations of the lambda-calculus.
• Interpretation of proofs and programs: interpretations of simply typed lambda-calculus and PCF in a closed Cartesian category (examples of CCC, adequacy theorem), categorical LL semantics and examples of models (Scott domains, relational semantics, vector models), interactive interpretations, adequacy theorems.
• Curry-Howard extensions: Curry-Howard for classical logic, extensions and variants of linear logic (light logics, differential logics, fixed point logics,...), probabilistic PCF (coherent probabilistic spaces and complete adequacy for probabilistic PCF)

Bibliography

• 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

• Bâtiment Sophie Germain
  8 place Aurélie Nemours
  75013 Paris