Bistructures, Bidomains and Linear Logic

Pierre-Louis Curien, Gordon Plotkin, Glynn Winskel

Abstract


Bistructures are a generalisation of event structures which allow
a representation of spaces of functions at higher types in an orderextensional setting. The partial order of causal dependency is replaced by two orders, one associated with input and the other with output in the behaviour of functions. Bistructures form a categorical model of Girard's classical linear logic in which the involution of linear logic is modelled, roughly speaking, by a reversal of the roles of input and output. The comonad of the model has an associated co-Kleisli category which is closely related to that of Berry's bidomains (both have equivalent non-trivial full sub-cartesian closed categories).

Full Text:

PDF


DOI: http://dx.doi.org/10.7146/brics.v4i15.18805
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.
OK


ISSN: 0909-0878 

Hosted by the State and University Library and Aarhus University Library