Advanced Topics in Semantics of Programming Languages

General Informations

• Course CR04 of the M2IF, ENS de Lyon.
• Schedule: on Wednesdays, 08:00 - 10:00.
• Lecturers:
  • Pierre Clairambault.
  • Colin Riba.
• Description:
  • The goal of this course is to bring students with basic knowledge in semantics of programming languages to a working knowledge of established tools and a perspective on active research topics.
    The course starts with basic tools in denotational semantics and logical relations for simply typed languages with general recursion. We then cover well established extensions to handle computational monads (typically for global state), recursive types and polymorphism. Finally, we survey some active research topics on algorithmic game semantics, Kripke logical relations and parametricity.

Courses

• Course 1 (11th Sept. 2019).
  
  • Introduction [slides].
  • Gödel's System T:
    • Definition.
    • Normalization: Statement of the inductive invariant.

• Course 2 (18th Sept. 2019).
  
  • Gödel's System T:
    • Proof of normalization.
    • Set-Theoretic Denotational Semantics.

• Course 3 (25th Sept. 2019).
  
  • PCF:
    • Definition [slides].
  • CPOs and Scott-continuity:
    • Definitions.
    • Continuous fonctions on flat natural numbers.
    • Basic closure properties (function space and direct product).

• Course 4 (2nd Oct. 2019).
  
  • CPOs and Scott-continuity:
    • Interpretation of PCF.
  • Computational Adequacy:
    • Definition of the Logical Relations.
    • The Saturation Lemma.

• Course 5 (9th Oct. 2019).
  
  • Computational Adequacy:
    • Statement and proof of the inductive invariant.
  • Exercises:
    • Continuity of the type 2 functions definable in Gödel's T.

• Course 6 (16th Oct. 2019).
  
  • Exercises:
    • Continuity of the type 2 functions definable in Gödel's T.

• Course 13 (11th Dec. 2019)
  • Girard-Reynolds System F [slides].

Research Articles

Polymorphism

• Polymorphism is not set-theoretic
  (J. C. Reynolds, 1984) [pdf].
  Notes:
  • An old classical result on the semantics of Girard-Reynolds System F.
  • For one person only.
  Choisi par Sébastien Michelland.

• Parametric Polymorphism and Operational Equivalence
  (A. M. Pitts, 2000) [pdf].
  Notes:
  • A nice development around parametricity.
  • Covers a lot of interesting techniques.

• Functorial Polymorphism
  (ES Bainbridge, PJ Freyd, A Scedrov, PJ Scott, 1990) [pdf].
  Notes:
  • Historically important paper on the link between polymorphism and natural tranformations.
  Choisi par Samuel Humeau.

Guarded Recursion

• A Modality for Recursion
  (H. Nakano, 2000) [ps].
  Notes:
  • A modal approach to general recursive types (and fixpoint combinators).
  • Extensions of this approach lead to categorical models for step indexing.
  • For one person only.
  Choisi par Isaac Ren.

Linear Logic

• Chapters 8 and 9 of Proofs and Types
  (J.-Y. Girard, P. Taylor and Y. Lafont, 1989) [pdf].
  Notes:
  • Chapter 8 introduces Coherence Spaces, an important class of domains which gave rise to Linear Logic.
  • Chapter 9 is an interpretation of System T in coherence spaces.
  • For one person only.
  Choisi par Nicolas Levy.

• Chapter 5 of the course notes Lambda-calcul: syntaxe et sémantique
  (T. Ehrhard, 2016) [pdf].
  Notes:
  • Covers the Scott model of Linear Logic.
  Choisi par Rémy Cerda.

• From Algol to Polymorphic Linear Lambda-calculus
  (P. O'Hearn and J. C. Reynolds, 2000) [ps.gz].
  Notes:
  • How linear logic can be used to analyse state.

• The Differential Lambda-Calculus
  (T. Ehrhard et L. Regnier, 2003) [pdf].
  Notes:
  • If you ever felt frustrated that you could not differentiate lambda-terms.

• Geometry of interaction 1: Interpretation of System F
  (J.-Y. Girard). Available on request.
  Notes:
  • Foundational paper for the Geometry of Interaction, a dynamic kind of denotational semantics with close links with Game Semantics.
  • Uses operator algebra, has had a lot of impact, but very challenging.

Game Semantics

• Innocent Game Semantics
  (R. Harmer, 2006) [pdf].
  
  • An introduction to Hyland-Ong game semantics.
  Choisi par Lison Blondeau.

• The regular-language semantics of second-order idealized ALGOL
  (D. Ghica and G. McCusker, 2003) [pdf].
  Notes:
  • How to automatically check equivalence of higher-order programs using game semantics
  • One person only.
  • A team of two could tackle the above along with the paper presenting the underlying fully abstract model:
    • Linearity, sharing and state: a fully abstract game semantics for idealized Algol with active expressions
      (Abramsky and McCusker, 1996) [pdf].
  Choisi par Rémy Neveu.

• Geometry of Synthesis: A structured approach to VLSI design
  (D. Ghica, 2007) [pdf].
  Notes:
  • How to compile hardware using game semantics.
  • One person only.
  Choisi par Pierre Marcus.

Topology

• Synthetic topology of data types and classical spaces
  (M. Escardo, 2004) [pdf].
  Notes:
  • Easy but very long.
  • Can be read by two persons.

• Chapter 10 Stone duality of the book Domains and Lambda-Calculi
  (R. Amadio and P.-L. Curien, CUP 46, 1998).
  Notes:
  • One can restrict to Sections 10.1-10.3.
  • For one person only.
  Choisi par Ugo Giocanti.

Continuation Passing Style and Classical Logic

• Call-by-Push-Value: A Subsuming Paradigm
  (P. B. Levy, 1999) [pdf].
  Notes:
  • Putting together call-by-name and call-by-value. If you are a fan of monads and adjunctions, this is for you.
  • At most one person.

• Disjunctive Tautologies as Synchronisation Schemes
  (V. Danos and J.-L. Krivine, 2000) [pdf].
  Notes:
  • A short and easy introduction to the computationl mechanism of Krivine's Classical Realizability.
  • For one person only.

• Control Categories and Duality: on the Categorical Semantics of the Lambda-Mu Calculus
  (P. Selinger, 2001) [pdf].
  Notes:
  • A dense but important work.
  • Sections 2-4 are difficult.
  • Sections 5-7 are more accessible.
  • Can be read by two persons, but splitting into 2-4 and 5-7 would be unfair.

Dependent Types

• Syntax and Semantics of Dependent Types
  (M. Hofmann, 1997) [pdf].
  Notes:
  • An introduction to the syntax and semantics of dependent types, which underly proof assistants like Coq.

Instrumentation of Semantics

• Using Models to Model-Check Recursive Schemes
  (S. Salvati and I. Walukiewicz) [pdf].
  Notes:
  • How to do model-checking with denotational models of the lambda-calculus.

• Normalization and Partial Evaluation
  (P. Dybjer and A. Filinski, 2002) [pdf].
  Notes:
  • How to normalize lambda-terms using semantics.
  • At least Sections 1-4.
  • Long but easy introductory paper on an important technique.
  • For one person only.
  Choisi par Nicolas Chappe.

Back home.