Reversible, Irreversible and Optimal λ-machines: Extended abstract

Vincent Danos, Laurent Regnier

Research output: Contribution to journalArticlepeer-review


There are two quite different possibilities for implementing linear head reduction in λ-calculus. Two ways which we are going to explain briefly here in the introduction and in details in the body of the paper. The paper itself is concerned with showing an unexpectedly simple relation between these two ways, which we term reversible and irreversible, namely that the latter may be obtained as a natural optimization of the former.
Original languageEnglish
Pages (from-to)40 - 60
Number of pages21
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 1996


  • reversible computations
  • λ-calculus
  • abstract machines
  • geometry of interaction


Dive into the research topics of 'Reversible, Irreversible and Optimal λ-machines: Extended abstract'. Together they form a unique fingerprint.

Cite this