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.