The geometry of interaction machine

ABSTRACT

We investigate implementation techniques arising directly from Girard's Geometry of Interaction semantics for Linear Logic, specifically for a simple functional programming language (PCF). This gives rise to a very simple, compact, compilation schema and run-time system. We analyse various properties of this kind of computation that suggest substantial optimisations that could make this paradigm of implementation not only practical, but potentially more efficient than extant paradigms.

REFERENCES

• ADLR94: Andrea Asperti, Vincent Danos, Cosimo Laneve, and Laurent Regnier. Paths in the A-calculus: Three years of communication without understanding. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 426-436. IEEE Computer Society Press, 1994.
• AJM94: Samson Abramsky , Pasquale Malacaria , Radha Jagadeesan, Full Abstraction for PCF, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.1-15, April 19-22, 1994
• AL91: Andrea Asperti and Cosimo Laneve. Interaction systems I: The theory of optimal reductions. TechnicM Report 1748, INRIA Rocquencourt, 1991.
• AL93: A. Asperti , C. Laneve, Interaction Systems II: The Practice of Optimal Reductions, University of Bologna, 1993
• Dan90: Vincent Danos. Une Applicat,on de la Logique Lindaire d l@tude des Processus de Normalisat,on (princ#palement du A-ealcul). PhD thesis, Universit# Paris VII, June 1990.
• DR93: Vincent Danos and Laurent Regnier. Local and asynchronous beta-reduction (an analysis of Girard's execution formula). In Proceedings, Eighth Annual IEEE Symposium on Logic zn Computer Science, pages 296-306. IEEE Computer Society Press, 1993.
• FH88: Anthony J. Field and Peter G. Harrison. Functional Programming. Addison Wesley, 1988.
• GAL92: Georges Gonthier , Martín Abadi , Jean-Jacques Lévy, The geometry of optimal lambda reduction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.15-26, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143172]
• Gir87: 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]
• Gir89a: Jean-Yves Girard. Geometry of interaction 1: Interpretation of System F. In R. Ferro et al., ed# itor, Logzc Colloquium 88. North Holland, 1989.
• Gir89b: Jean-Yves Girard. Towards a geometry of interaction. In J. W. Gray and Andre Scedrov, editors, Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 69-108. American Mathematical Society, 1989.
• Laf90: Yves Lafont, Interaction nets, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.95-108, December 1989, San Francisco, California, United States [doi>10.1145/96709.96718]
• Lan64: Peter J. Landin. The mechanical evaluation of expressions. Computer Journal, 6:308-320, 1964.
• Lev80: Jean-Jacques Levy. Optimal reductions in the lambda calculus. In J.P. Hindley and J.R Seldin, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 159-191. Academic Press, 1980.
• Mac94: Inn Mackie. The Geometry of Implementation. PhD thesis, Department of Computing, Imperim College of Science Technology and Medicine, 1994.
• Pey87: Simon L. Peyton Jones, The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science), Prentice-Hall, Inc., Upper Saddle River, NJ, 1987
• Plo77: Gordon Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223-255, 1977.
• Wad71: Christopher P. Wadsworth. Semantics and Pragmatics of the Lambda-Calculus. PhD thesis, Oxford University, 1971.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Languages