Bistructures, Bidomains and Linear Logic

Pierre-Louis Curien
Gordon Plotkin
Glynn Winskel

June 1997


Bistructures are a generalisation of event structures which allow a representation of spaces of functions at higher types in an order-extensional 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)

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.