## Emulating linear types in Haskell

Institute of Cybernetics at TUT

Thursday, 16 February 2012, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**Abstract**: The distinguishing feature of linear logic is that
each hypothesis must be used exactly once during reasoning. Applying a
Curry-Howard isomorphism to linear logic leads to a programming
calculus that allows the user to represent the state of real world
objects as purely functional values. A variation of this idea has been
implemented in the Clean programming language, allowing it to deal
with side effects in a more functional way than Haskell does. This
talk shows that linear types can be emulated in Haskell. The key idea
is to implement a categorical model of linear logic using Haskell's
arrow framework.

Tarmo Uustalu

Last update 16.2.2012