Girard's Geometry of Interaction (GoI) develops a mathematical framework for modelling the dynamics of cut elimination. We introduce a typed version of GoI, called Multiobject GoI for both multiplicative linear logic (MLL) and multiplicative exponential linear logic (MELL) with units. We present a categorical setting that includes our previous (untyped) GoI models, as well as more general models based on monoidal *-categories. Our development of multiobject GoI depends on a new theory of partial traces and trace classes, which we believe is of independent interest, as well as an abstract notion of orthogonality (which is related to work of Hyland and Schalk). We develop Girard's original theory of types, data and algorithms in our setting, and show his execution formula to be an invariant of cut elimination (under some restrictions). We prove soundness theorems for the MGoI interpretation (for Multiplicative and Multiplicative Exponential Linear Logic) in partially traced *-categories with an orthogonality. Finally, we briefly discuss the relationship between our GoI interpretation and other categorical interpretations of GoI.

We present an axiomatic framework for Girard's Geometry of Interaction based on the notion of linear combinatory algebra. We give a general construction on traced monoidal categories, with certain additional structure, that is sufficient to capture the exponentials of Linear Logic, which produces such algebras (and hence also ordinary combinatory algebras). We illustrate the construction on six standard examples, representing both the ‘particle-style’ as well as the ‘wave-style’ Geometry of Interaction.