Interaction nets
Yves Lafont · 1990
We propose a new kind of programming language, with the following features:a simple graph rewriting semantics,a complete symmetry between constructors and destructors,a type discipline for deterministic and deadlock-free (microscopic) parallelism.Interaction nets generalize Girard's proof nets of linear logic and illustrate the advantage of an integrated logic approach, as opposed to the external one. In other words, we did not try to design a logic describing the behaviour of some given computational system, but a programming language for which the type discipline is already (almost) a logic.In fact, we shall scarcely refer to logic, because we adopt a naive and pragmatic style. A typical application we have in mind for this language is the design of interactive softwares such as editors or window managers.