Operational interpretations of linear logic

Two different operational interpretations of intuitionistic linear logic ha ve been proposed in the literature. The simplest interpretation recomputes non-linear values every time they are required. It has good memory-manageme nt properties, but is often dismissed as being too inefficient. Alternative ly, one can memoize the results of evaluating non linear values. This avoid s any recomputation, but has weaker memory-management properties. Using a n ovel combination of type-theoretic and operational techniques we give a con cise formal comparison of the two interpretations. Moreover, we show that t here is a subset of linear logic where the two operational interpretations coincide. In this subset, which is sufficiently expressive to encode call-b y-value lambda-calculus, we can have the best of both worlds: a simple and efficient implementation, and good memory-management properties. (C) 1999 E lsevier Science B.V. All rights reserved.