Abstract

We present a linear abstract machine based on a calculus with explicit substitutions. We exploit the distinction between intuitionistic and linear variables in Barber and Plotkin's DILL (Dual Intuitionistic Linear Logic) to construct a machine which extends Krivine's machine by adding a machine for linear types on top of it. This separation makes it easy to show that this machine has the single pointer property: each variable of linear type has exactly one pointer to it. We also present an algorithm for translating lambda-terms into linear lambda-terms which tries to preserve linearity as much as possible.

This is joint work with Francisco Alberti, Neil Ghani and Valeria de Paiva.