Bistructures, Bidomains and Linear Logic

Abstract

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).