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.