A categorical model for the geometry of interaction

Abstract: 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. [Copyright &y& Elsevier]