# Models of programming languages: Domains, Categories, Games (M2 MPRI)

## Lecture 1: Introduction

Teacher: Paul-André Melliès

## Lecture 2: Introduction to Domain theory

Teacher: Paul-André Melliès

## Lecture 3: Cartesian closed categories

Teacher: Paul-André Melliès

## Execises 2: Stable models of $λ$-calculus

Teacher: Paul-André Melliès

## Lecture 4: Simply typed λ-calculus as CCC

Teacher: Paul-André Melliès

## Lecture 5: Coherence spaces

Teacher: Paul-André Melliès

## Lecture 6: Monoidal Categories

Teacher: Paul-André Melliès

## Lecture 7: Step functions and exponential modalities

Teacher: Paul-André Melliès

## Lecture 8:

Teacher: Paul-André Melliès

## Lecture 9: Lazy PCF

Teacher: Thomas Ehrhard

## Execises 3: Coherence spaces and lazy integers

Teacher: Thomas Ehrhard

## Lecture 10: Categorical combinators, Categorical Abstract Machines

Teacher: Pierre-Louis Curien

## Lecture 11: Categorical model of LL and Eilenberg-Moore category of $!$

Teacher: Thomas Ehrhard

## Lecture 12: $PoL$, $PoLR$, $PoC$ categories

Preorders S = (\underbrace{\vert S \vert}_{\text{set}}, \underbrace{≤_S}_{\text{refl. trans. rel. on } \vert S \vert})

## Lecture 13: Scott semantics

Preorders and linear functions (Scott semantics)

Full Abstraction

## Realisability, $PoLR_!$ not fully abstract

Φ = (x_1: u^1: A_1, …, x_n: u^n: A_n)\\ \underline Φ = (x_1: A_1, …, x_n: A_n)

## Concrete Data Structures, Sequential functions

Sequential ⟹ Stable Cds M = (\underbrace{C}_{\text{cells}}, \underbrace{V}_{\text{values}}, \underbrace{E}_{⊆ C × V \text{ = events}}, \underbrace{⊢}_{\...

Reminder:

## PCF Böhm trees

$λ$-calculus: Normal forms of the form

II.