Typed GoI for Exponentials
In a recent paper we introduced a typed version of Geometry of Interaction, called the Multi-object Geometry of Interaction (MGoI). Using this framework we gave an interpretation for the unit-free multiplicative fragment of linear logic. In this paper, we extend our work to cover the exponentials. We introduce the notion of a Got Category that embodies the necessary ingredients for an MGoI interpretation for unit-free multiplicative and exponential linear logic.