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: