The Geometry of Interaction Machine

Abstract

We investigate implementation techniques arising directly from Girard's Geometry of Interaction semantics for Linear Logic, specifically for a simple functional programming language (PCF). This gives rise to a very simple, compact, compilation schema and run-time system. We analyse various properties of this kind of computation that suggest substantial optimisations that could make this paradigm of implementation not only practical, but potentially more efficient than extant paradigms.