November 26th. Introduction on Linear Logic. Speaker: Thomas Seiller.

December 8, 13-15 in 2A14. Introduction to Linear Logic II. Speaker: Thomas Seiller.

December 15, 13-15 in 2A14. Categorical Semantics of Linear Logic. Speaker: Jonas Frey.

January 26, 13-15 in TBA. Categorical Semantics of Linear Logic, Ctd. Speaker: Jonas Frey.

February 2, 13-15 in 4A58. Proof nets. Speaker: Thomas Seiller.

February 9, 13-15 in 4A58. Differential linear logic. Speaker: Marie Kerjean.

February 16, 13-15 in 4A58. Differential linear logic II. Speaker: Marie Kerjean.

February 23, 13-15 in 4A58. Complexity and linear logic. Speaker: Thomas Seiller.

March 1, 13-15 in 4A58. Geometry of interaction. Speaker: Thomas Seiller.

March 8, 13-15 in 4A58. Geometry of interaction II. Speaker: Thomas Seiller.

April 5, 13-15 in 4A58. Introduction to realizability toposes, Part 1. Speaker: Jonas Frey.

Suggested references

Domain theory:

Outline of a mathematical theory of computation (Scott 1970) is probably the best starting point,

Continuous Lattices (Scott 1971) provides the domains constructions;

Data types as lattices (Scott 1976) shows that there is a semantics of lambda-calculus (in fact PCF) in the domain of subsets of natural numbers (hence it provides a model of reasonable size)

Stable models of the typed lambda-calculus (Berry 1978) introduces the notion of stability [it might be quite difficult to get your hands on it, you can just ask Thomas for a copy of it].

Towards a mathematical semantics for computer languages (Scott and Strachey 1971)

Normal functors:

Normal functors, power series and the lambda-calculus (Girard 1988). Note that it uses old category theory terminology and a modernised version would be much easier to read

Two applications of analytic functors (Hasegawa 2002); this is a more recent paper in which one can find details about the analytic functors model of lambda-calculus.

## Meetings

## Suggested references

## Domain theory:

## Normal functors: