Laurent Regnier

From Girard's Geometry of Interaction to Krivine's Abstract Machine

We first design the Interaction Abstract Machine (IAM) for executing multiplicative-exponential nets as a bideterministic automaton based on the geometry of interaction. In a second stage we define an optimization of the IAM based on the geometry of regular paths as it has been analysed by the legality condition of Asperti and Laneve; this yields the Jumping Abstract Machine (JAM). Then restricting nets to those coming from the translation of lambda-calculus, we show that the JAM is exactly the Krivine's machine for executing lambda-terms.