General Informations
 Course CR14 of the M2IF, ENS de Lyon.
 Schedule: on Tuesdays, 10:15  12:15.
 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. 2018).
 Introduction [slides].
 Gödel's System T: Definition.

Course 2 (18th Sept. 2018).
 Gödel's System T: Normalization.

Course 3 (25th Sept. 2018)
[slides].
 Gödel's System T: SetTheoretic Denotational Semantics.
 PCF: Definition.

Course 4 (2nd Oct. 2018)
 Denotational Semantics of PCF [slides].

Course 9 (20 Nov. 2018)
 D_{∞} Models.

Course 10 (4 Dec. 2018)
 GirardReynolds System F [slides].
Research Articles
Polymorphism

An Ideal Model of Recursive Polymorphic Types
(D. MacQueen, G. Pltokin and R. Sethi, 1986) [pdf]. A bit old, but interesting techniques for an important problem.

Semantic Types: A Fresh Look at the Ideal Model for Types
(J. Vouillon and P.A. Melliès, 2004) [ps]. Toward a modern reading of the above article.

Theorems for free!
(P. Wadler, 1989) [pdf].
Notes: Short classic. Explains the notion of parametricity.
 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.
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.

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].
 If you ever felt frustrated that you could not differentiate lambdaterms.
Games Semantics

Game Semantics
(M. Hyland, 1997) [pdf].
Notes: Excellent chapter on the basics of game semantics.
 Uses some Linear Logic.
 If chosen by one person, then covering Sections 13 is sufficient.

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, sharingand state: a fully abstract game semantics for idealized Algol with active expressions" by Abramsky and McCusker. [pdf].

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.
Continuation Passing Style and Classical Logic

CallbyPushValue: A Subsuming Paradigm
(P. B. Levy, 1999) [pdf]
 Putting together callbyname and callbyvalue. If you are a fan of monad s 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.

Chapters 1 and 2 of
Homotopy Type Theory: Univalent Foundations of Mathematics
(2013) [pdf].
Notes: Be prepared for the next new foundations of mathematics!
Instrumentation of Semantics

A Finite Semantics of SimplyTyped Lambda Terms for Infinite Runs of Automata.
(K. Aehlig, 2006) [pdf].
 How to do modelchecking with models of the lambdacalculus!
 At most one person.

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.