Archive 2022
Program requirementsexamen
TeacherAntonio Bucciarelli and Claudia Faggian
Weekly hours 4 h CM
Years Master Logique Mathématique et Fondements de l'Informatique M2 Logos

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 programs, 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 some more recent developments.

Contents

The first part of the course focuses on the denotational semantics of functional programming, the second one on the operational semantics. Both build on proof theory and the theory of lambda-calculus.

First half :
  • Interpretation of proofs and programs: interpretations of simply typed lambda-calculus and PCF in a closed Cartesian category (examples of CCC, adequacy theorem).
  • Examples of models (Scott domains, coherence spaces, game models).
  • Definability and full abstraction problems.
  • Logical relations.
Second half :
  • Tools to analyze the operational properties of a system: Abstract Rewriting Theory.
  • Induction and Co-induction proof principles.
  • Bridging between lambda-calculus and functional programming. Call-by-Value and Call-by Name, weak and lazy calculi. Big-Step and Small-Step operational semantics. Observational equivalence.
  • Reasoning on programs equivalence . Bisimulation and coinductive methods.
  • Linear Logic and Proof-Nets.
  • Beyond pure: Probabilistic lambda-calculi.

Bibliography

  • 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)