Encoding left reduction in the λ-calculus with interaction nets
Sylvain Lippi · Mathematical Structures in Computer Science · 2002
This paper presents a simple implementation of the λ-calculus in the interaction net paradigm. It is based on a two-fold translation. λ-terms are coded (for duplication) or decoded (for execution), and reduction is achieved by switching between these two states: decoding corresponds to head reduction and encoding to left reduction.