Interaction nets

ABSTRACT

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 naïve 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.

REFERENCES

• Girard87: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• Girard88: J.Y. Girard, Multiplicatives, in Rendiconti del seminario ma~ematico dell'universi~ e politecnico di Torino, special issue on logic and computer science (1988).
• Girard89: J.Y. Girard, Towards a geometry of interaction, in Conference on categories, computer science and loqic, Contempory Mathematics, AMS 92 (1989).
• Girard89a: J.Y. Girard, Geometry of interaction 1: interpretation of system F, in ASL meeting (North- Holland, Padova, 1989).
• Girafont: J. Y. Girard , Y. Lafont, Linear logic and lazy computation, II and Colloquium on Functional and Logic Programming and Specifications (CFLP) on TAPSOFT '87: Advanced Seminar on Foundations of Innovative Software Development, p.52-66, March 1987, Pisa, Italy
• Giraflor: Jean-Yves Girard , Paul Taylor , Yves Lafont, Proofs and types, Cambridge University Press, New York, NY, 1989
• Lafont87: Y. Lafont, Linear Logic Programming, in Workshop on Programming Logic (GSteborg, 1987) 2O9-220.
• Lafont88: Y. Lafont, Logiques, Cat6gories et Machines, th~se de doctorat (Universit6 de Paris VII, 1988).
• Lafont88a: Y. Lafont, The linear abstract machine, Theoretical Computer Science, v.59 n.1-2, p.157-180, July 1988 [doi>10.1016/0304-3975(88)90100-4]
• Regnos: V. Danos & L. R~gnier, The structure of muttiplicatives, typescript (1988).

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Algorithms, Languages, Theory