Memoryful geometry of interaction

Abstract

Girard's Geometry of Interaction (GoI) is interaction based semantics of linear logic proofs and, via suitable translations, of functional programs in general. Its mathematical cleanness identifies essential structures in computation; moreover its use as a compilation technique from programs to state machines---"GoI implementation," so to speak---has been worked out by Mackie, Ghica and others. In this paper, we develop Abramsky's idea of resumption based GoI systematically into a generic framework that accounts for computational effects (nondeterminism, probability, exception, global states, interactive I/O, etc.). The framework is categorical: Plotkin & Power's algebraic operations provide an interface to computational effects; the framework is built on the categorical axiomatization of GoI by Abramsky, Haghverdi and Scott; and, by use of the coalgebraic formalization of component calculus, we describe explicit construction of state machines as interpretations of functional programs. The resulting interpretation is shown to be sound with respect to equations between algebraic operations, as well as to Moggi's equations for the computational lambda calculus. We illustrate the construction by concrete examples.