Linear logic with boxes

Interaction nets provide a graphical paradigm of computation based on net rewriting. By encoding the cut-elimination process of linear logic they have proved successful in understanding the dynamics of reduction in the λ-calculus. G. Gonthier et al. (1992) gave an optimal infinite system of interaction nets for linear logic by removing the global boxes. However efficient implementations of optimal reduction have had to break away from the interaction net paradigm. Here we give an efficient new finite interaction net encoding of linear logic which is not optimal, but overcomes many of the inefficiencies caused by the bookkeeping operations in the implementations of optimal reduction. We code the global operations on boxes (contraction, weakening, dereliction, commutative cut) in a local way, keeping the box structure, which results in a system allowing a great deal of sharing with an extremely low overhead. We believe that this implementation is the most faithful of all the extant interaction net encodings of linear logic