A categorical model for the geometry of interaction

We consider the multiplicative and exponential fragment of linear logic (MELL) and give a geometry of interaction (GoI) semantics for it based on unique decomposition categories. We prove a soundness and finiteness theorem for this interpretation. We show that Girard's original approach to GoI 1 via operator algebras is exactly captured in this categorical framework. (c) 2005 Elsevier B.V. All rights reserved.