| Bistructures, Bidomains and Linear Logic (2007) | |||||||||||||||
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). 1 Introduction In this paper we link Winskel's bistructures [25], Girard's linear logic [10] and Berry's bidomains [25]. We show how bistructures provide a model of classical linear logic extending Girard's web model [10, 11]; we show too that a certain class of bistructures represent bidomains. We hope that the ... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||