Categorical semantics for linear logic

Wolfgang Jeltsch

Institute of Cybernetics at TUT

Tuesday, 18 June 2013, 14:00 (note the unusual weekday)
Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

Abstract: The distinguishing feature of linear logic is that each proposition must be used exactly once in a proof. As a result, linear logic provides a straightforward way to reason about resources. Interpreted as a programming language, linear logic makes it possible to deal with mutable state in a purely functional manner.

In this talk, I first give a short introduction to linear logic and present a categorical semantics for it. Afterwards, I show how linear and non-linear logic can interact and how this interaction can be modeled categorically via adjunctions.


Tarmo Uustalu
Last update 19.6.2013