Reversible, Irreversible and Optimal lambda-Machines.

Vincent Danos, Laurent Regnier

Research output: Contribution to journalArticlepeer-review


Lambda-calculus is the core of functional programming, and many different ways to evaluate lambda-terms have been considered. One of the nicest, from the theoretical point of view, is head linear reduction.

We compare two ways of implementing that specific evaluation strategy: “Krivine's abstract machine” and the “interaction abstract machine”. Runs on those machines stand in a relation which can be accurately described using the call/return symmetry discovered by Asperti and Laneve.
Original languageEnglish
Pages (from-to)79-97
Number of pages19
JournalTheoretical Computer Science
Issue number1-2
Publication statusPublished - Sep 1999


  • λ-calculus
  • Linear logic
  • Linear head reduction
  • Abstract machines
  • Geometry of interaction
  • Reversible computations


Dive into the research topics of 'Reversible, Irreversible and Optimal lambda-Machines.'. Together they form a unique fingerprint.

Cite this