Seminar on Semantics of Linear Logic

Meetings

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