Operational interpretations of linear logic

David N. Turner, Philip Wadler

Research output: Contribution to journalArticlepeer-review

Abstract

Two different operational interpretations of intuitionistic linear logic have been proposed in the literature. The simplest interpretation recomputes non-linear values every time they are required. It has good memory-management properties, but is often dismissed as being too inefficient. Alternatively, one can memoize the results of evaluating non-linear values. This avoids any recomputation, but has weaker memory-management properties. Using a novel combination of type-theoretic and operational techniques we give a concise formal comparison of the two interpretations. Moreover, we show that there is a subset of linear logic where the two operational interpretations coincide. In this subset, which is sufficiently expressive to encode call-by-value lambda-calculus, we can have the best of both worlds: a simple and efficient implementation, and good memory-management properties.
Original languageEnglish
Pages (from-to)231 - 248
JournalTheoretical Computer Science
Volume227
Issue number1-2
DOIs
Publication statusPublished - 1999

Fingerprint Dive into the research topics of 'Operational interpretations of linear logic'. Together they form a unique fingerprint.

Cite this