An abstract machine for Lambda-terms normalization

ABSTRACT

Two abstract machines reducing terms to their full normal form are presented in this paper. They are based on Krivine's abstract machine [Kri85] which uses an environment to store arguments of function calls. A proof of their correctness is then stated in the abstract framework of &lgr;&sgr;-calculus [Cur89].

REFERENCES

• ACCL90: M. Abadi , P. L. Curien , J. J. Levy, Explicit substitutions, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.31-46, December 1989, San Francisco, California, United States [doi>10.1145/96709.96712]
• App87: Andrew W. Appel. Reopening Closures. Technical Report TR 079-87, Princeton university, 1987.
• Arg89: Guy Argo, Improving the three instruction machine, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.100-115, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99378]
• Bar75: H.P. Barendregt.The type free A-calculus. Technical Report, Utrecht University and ETH Zurich, 1975.
• Bar81: H. Barendregt. The Lambda Calculus. North Holland, 1981.
• BBKV76: H.P. Barendregt, J. Bergstra, J.W. Klop, and H. Volken. Degrees, reductions and representability in the A-calculus. Technical Report 22, University of Utrecht, 1976.
• BD77: R. M. Burstall , John Darlington, A Transformation System for Developing Recursive Programs, Journal of the ACM (JACM), v.24 n.1, p.44-67, Jan. 1977 [doi>10.1145/321992.321996]
• CCMS86: Guy Cousineau, Pierre-Louis Curien, Michel Mauny, and Ascander Sukrez. Combinateurs Catdgoriques ~t lmpldmentation des Langages fonctionnels. Technical Report 86-3, LIENS, 1986.
• Cur89: Pierre-Louis Curien. The strong calculus of closures or Act-calculus a short note. 1989.
• FW87: Jon Fairbairn , Stuart Wray, TIM: A simple, lazy abstract machine to execute supercombinatorics, Proceedings of the Functional Programming Languages and Computer Architecture, p.34-45, September 14-16, 1987
• HL86: T Hardin , A Laville, Proof of termination of the rewriting system SUBST on CCL, Theoretical Computer Science, v.46 n.2-3, p.305-312, Oct. 1986
• Kri85: Jean-Louis Krivine. Un interpr~teur du X-calcul. 1985.
• Lev78: Jean-Jacques L~vy. R~ductions correctes et optimales dana le lambda-calcul. PhD thesis, Universit/~ Paris VII, 1978.
• Moh86: Christine M ohring. Exemples de d~velopement de Programmes duns la Th~orie des Constructions. Technical Report 497, INRIA, 1986.
• NW90: Gopalan Nadathur , Debra Sue Wilson, A representation of Lambda terms suitable for operations on their intensions, Proceedings of the 1990 ACM conference on LISP and functional programming, p.341-348, June 27-29, 1990, Nice, France [doi>10.1145/91556.91682]
• PJ87: Simon Peyton-Jones. Implementation of Functional Programming Languages. Prentice Hall, 1987.
• Plo81: Gordon D. Plotkin. A Structural Approach to Operational semantics. Technical Report DAIMI FN-19, Aarhus University, 1981.
• Wad88: Philip Wadler, Deforestation: transforming programs to eliminate trees, Proceedings of the Second European Symposium on Programming, p.231-248, January 1988, Nancy, France

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Operations on languages

General Terms:
Algorithms, Languages, Theory