An Explicit Framework for Interaction Nets

Interaction nets are a graphical formalism inspired by Linear Logicproof-nets often used for studying higher order rewriting e.g. \Beta-reduction.Traditional presentations of interaction nets are based on graph theory andrely on elementary properties of graph theory. We give here a more explicitpresentation based on notions borrowed from Girard's Geometry of Interaction:interaction nets are presented as partial permutations and a composition ofnets, the gluing, is derived from the execution formula. We then definecontexts and reduction as the context closure of rules. We prove strongconfluence of the reduction within our framework and show how interaction netscan be viewed as the quotient of some generalized proof-nets