Abstract
Token-passing nets were proposed by Sinot as a simple mechanism for encoding evaluation strategies for the ?-calculus in interaction nets. This work extends token-passing nets to cover a typed functional language equipped with structured types and unrestricted recursion. The resulting interaction system is derived systematically from the chosen big-step operational semantics. Along the way, we actually characterize and discuss several design decisions of token-passing nets and extend them in order to achieve simpler interaction net systems with a higher degree of embedded parallelism.

Abstract
This paper is a formal study of how to implement interaction nets, filling an important gap in the work on this graphical rewriting formalism, very promising for the implementation of languages based on the gimel -calculus. We propose the first abstract machine for interaction net reduction, based on a decomposition of interaction rules into more atomic steps, which tackles all the implementation details hidden in the graphical presentation. As a natural extension of this, we then give a concurrent shared-memory abstract machine, and show how to implement it, resulting in the first parallel implementation of interaction nets.

Abstract

Abstract

Abstract
An examination of Girard's execution formula suggests implementations of the Geometry of Interaction at the syntactic level. In this paper we limit our scope to ground-type terms and study the parallel aspects of such implementations, by introducing a family of abstract machines which can be directly implemented. These machines address all the important implementation issues such as the choice of an interthread communication model, and allow to incorporate specific strategies for dividing the computation of the execution path into smaller tasks.

Abstract
This paper presents a formalism for defining higher-order systems based on the notion of graph transformation (by rewriting or interaction). The syntax is inspired by the Combinatory Reduction Systems of Klop. The rewrite rules can be used to define first-order systems, such as graph or term-graph rewriting systems, Lafont's interaction nets, the interaction systems of Asperti and Laneve, the non-deterministic nets of Alexiev, or a process calculus. They can also be used to specify higher-order systems such as hierarchical graphs and proof nets of Linear Logic, or to specify the operational semantics of graph-based languages.