## Categorical semantics for linear logic

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.

References:

- P. N. Benton.
A mixed linear and non-linear logic: Proofs, terms and models.
Technical Report UCAM-CL-TR-352,
University of Cambridge, Oct. 1994.
link

Tarmo Uustalu

Last update 19.6.2013