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. Key words: Geometry of Interaction, Traced monoidal categories, Linear logic, Partially additive categories, Unique decomposition categories.

• Type: Conference
• Year: 2004
• Where: ICALP
• Authors: Esfandiar Haghverdi, Philip J. Scott
• Keywords: Girard’s Original Approach, ICALP 2004, Linear Logic, Theoretical Computer Science, Unique Decomposition Categories