Reversible, Irreversible and Optimal λ-machines
Vincent Danos, Laurent Régnier · Electronic Notes in Theoretical Computer Science · 1996
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.