Result of feedback form submitted by
Ritter (E.Ritter@cs.bham.ac.uk) on Monday, August 10, 1998 at 15:14:21
---------------------------------------------------------------------------

Contributions offered by Eike Ritter for topics 
F (games, sequentiality, and abstract machines),
H (semantics-based optimisation)

We present a linear abstract machine based on a calculus with explicit
substitutions. We exploit the distinction between intuitionistic and
linear variables in 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.