An abstract machine for Lambda-terms normalization

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

An abstract machine for Lambda-terms normalization

Full text

Pdf (746 KB)

Source

Conference on LISP and Functional Programming archive
Proceedings of the 1990 ACM conference on LISP and functional programming table of contents

Nice, France

Pages: 333 - 340

Year of Publication: 1990

ISBN:0-89791-368-X

Author

P. Crégut

LIENS CNRS U.R.A. 1327, 45 rue d'Ulm 75230 Paris CEDEX 5 France

Sponsors

INRIA : Institut Natl de Recherche en Info et en Automatique
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGART: ACM Special Interest Group on Artificial Intelligence
SIGPLAN: ACM Special Interest Group on Programming Languages
SIGSAM: ACM Special Interest Group on Symbolic and Algebraic Manipulation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 8, Downloads (12 Months): 31, Citation Count: 13

Additional Information:

abstract references cited by index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/91556.91681 What is a DOI?

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

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked 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

CITED BY 13

	Thérèse Hardin , Luc Maranget , Bruno Pagano, Functional back-ends within the lambda-sigma calculus, ACM SIGPLAN Notices, v.31 n.6, p.25-33, June 15, 1996
	Mads Sig Ager , Dariusz Biernacki , Olivier Danvy , Jan Midtgaard, A functional correspondence between evaluators and abstract machines, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.8-19, August 27-29, 2003, Uppsala, Sweden
	Benjamin Grégoire , Xavier Leroy, A compiled implementation of strong reduction, ACM SIGPLAN Notices, v.37 n.9, p.235-246, September 2002
	Mads Sig Ager , Olivier Danvy , Jan Midtgaard, A functional correspondence between call-by-need evaluators and lazy abstract machines, Information Processing Letters, v.90 n.5, p.223-232, 15 June 2004
	Olivier Danvy, Editorial, Higher-Order and Symbolic Computation, v.20 n.3, p.197-198, September 2007
	Mitchell Wand, On the correctness of the Krivine machine, Higher-Order and Symbolic Computation, v.20 n.3, p.231-235, September 2007
	Rémi Douence , Pascal Fradet, The next 700 Krivine machines, Higher-Order and Symbolic Computation, v.20 n.3, p.237-255, September 2007
	Daniel P. Friedman , Abdulaziz Ghuloum , Jeremy G. Siek , Onnie Lynn Winebarger, Improving the lazy Krivine machine, Higher-Order and Symbolic Computation, v.20 n.3, p.271-293, September 2007
	David A. Schmidt, State-transition machines, revisited, Higher-Order and Symbolic Computation, v.20 n.3, p.333-335, September 2007
	Magorzata Biernacka , Olivier Danvy, A syntactic correspondence between context-sensitive calculi and abstract machines, Theoretical Computer Science, v.375 n.1-3, p.76-108, May, 2007
	F.-R. Sinot, Call-by-need in token-passing nets, Mathematical Structures in Computer Science, v.16 n.4, p.639-666, August 2006
	Peter Sestoft, Deriving a lazy abstract machine, Journal of Functional Programming, v.7 n.3, p.231-264, May 1997
	Małgorzata Biernacka , Olivier Danvy, A concrete framework for environment machines, ACM Transactions on Computational Logic (TOCL), v.9 n.1, p.6-es, December 2007