General Informations
 Course CR04 of the M2IF, ENS de Lyon.
 Schedule: on Wednesdays, 08:00  10:00.
 Lecturers:

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.

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.
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.
 SetTheoretic Denotational Semantics.

Gödel's System T:

Course 3 (25th Sept. 2019).

PCF:
 Definition [slides].

CPOs and Scottcontinuity:
 Definitions.
 Continuous fonctions on flat natural numbers.
 Basic closure properties (function space and direct product).

PCF:

Course 4 (2nd Oct. 2019).

CPOs and Scottcontinuity:
 Interpretation of PCF.

Computational Adequacy:
 Definition of the Logical Relations.
 The Saturation Lemma.

CPOs and Scottcontinuity:

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.

Computational Adequacy:

Course 6 (16th Oct. 2019).

Exercises:
 Continuity of the type 2 functions definable in Gödel's T.

Exercises:

Course 13 (11th Dec. 2019)
 GirardReynolds System F [slides].
Research Articles
Polymorphism

Polymorphism is not settheoretic
(J. C. Reynolds, 1984) [pdf].
Notes: An old classical result on the semantics of GirardReynolds System F.
 For one person only.

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.
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.
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.

Chapter 5 of the course notes
Lambdacalcul: syntaxe et sémantique
(T. Ehrhard, 2016) [pdf].
Notes: Covers the Scott model of Linear Logic.

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

The Differential LambdaCalculus
(T. Ehrhard et L. Regnier, 2003) [pdf].
Notes: If you ever felt frustrated that you could not differentiate lambdaterms.

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 HylandOng game semantics.

The regularlanguage semantics of secondorder idealized ALGOL
(D. Ghica and G. McCusker, 2003) [pdf].
Notes: How to automatically check equivalence of higherorder 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].

Linearity,
sharing and state: a fully abstract game semantics for idealized
Algol with active expressions

Geometry of Synthesis: A structured approach to VLSI design
(D. Ghica, 2007) [pdf].
Notes: How to compile hardware using game semantics.
 One person only.
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 LambdaCalculi
(R. Amadio and P.L. Curien, CUP 46, 1998).
Notes: One can restrict to Sections 10.110.3.
 For one person only.
Continuation Passing Style and Classical Logic

CallbyPushValue: A Subsuming Paradigm
(P. B. Levy, 1999) [pdf].
Notes: Putting together callbyname and callbyvalue. 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 LambdaMu Calculus
(P. Selinger, 2001) [pdf].
Notes: A dense but important work.
 Sections 24 are difficult.
 Sections 57 are more accessible.
 Can be read by two persons, but splitting into 24 and 57 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 ModelCheck Recursive Schemes
(S. Salvati and I. Walukiewicz) [pdf].
Notes: How to do modelchecking with denotational models of the lambdacalculus.

Normalization and Partial Evaluation
(P. Dybjer and A. Filinski, 2002) [pdf].
Notes: How to normalize lambdaterms using semantics.
 At least Sections 14.
 Long but easy introductory paper on an important technique.
 For one person only.
Back home.