de Mathématiques de Luminy
Encoding left reduction in the lambda-calculus with interaction nets
This paper presents a simple implementation of the lambda-calculus in the interaction net paradigm. It is based on a two-fold translation. Lambda-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.