|Teacher||Claudia Faggian and Gabriele Vanoni|
|Years||Master Logique Mathématique et Fondements de l'Informatique M2 Logos|
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.
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 :
- Introduction to the Agda proof assistant, de Bruijn notation, and
recap on the untyped lambda-calculus.
- The denotational semantics of the untyped lambda-calculus, formalized.
- Soundness and adequacy, formalized.
- Contextual equivalence, filter models, and intersection types.
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.
- Wadler, Philip, Wen Kokke, and Jeremy G. Siek. Programming Language Foundations in Agda. Available at https://plfa.inf.ed.ac.uk/22.08/. 2022.
- R. AMADIO : Operational methods in semantics (available on HAL https://hal.archives-ouvertes.fr/cel-01422101v1).
- D. SANGIORGI: Introduction to Bisimulation and Coinduction (Cambridge University Press, 2011)