Definitional interpreters for higher-order programming languages

ABSTRACT

Higher-order programming languages (i.e., languages in which procedures or labels can occur as values) are usually defined by interpreters which are themselves written in a programming language based on the lambda calculus (i.e., an applicative language such as pure LISP). Examples include McCarthy's definition of LISP, Landin's SECD machine, the Vienna definition of PL/I, Reynolds' definitions of GEDANKEN, and recent unpublished work by L. Morris and C. Wadsworth. Such definitions can be classified according to whether the interpreter contains higher-order functions, and whether the order of application (i.e., call-by-value versus call-by-name) in the defined language depends upon the order of application in the defining language. As an example, we consider the definition of a simple applicative programming language by means of an interpreter written in a similar language. Definitions in each of the above classifications are derived from one another by informal but constructive methods. The treatment of imperative features such as jumps and assignment is also discussed.

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.

	1	John McCarthy, Recursive functions of symbolic expressions and their computation by machine, Part I, Communications of the ACM, v.3 n.4, p.184-195, April 1960 [doi>10.1145/367177.367199]
	2	P. J. Landin, The next 700 programming languages, Communications of the ACM, v.9 n.3, p.157-166, March 1966 [doi>10.1145/365230.365257]
	3	Arthur Evans, Jr., PAL—a language designed for teaching programming linguistics, Proceedings of the 1968 23rd ACM national conference, p.395-403, August 27-29, 1968 [doi>10.1145/800186.810604]
	4	John C. Reynolds, G/EDANKEN—a simple typeless language based on the principle of completeness and the reference concept, Communications of the ACM, v.13 n.5, p.308-319, May 1970 [doi>10.1145/362349.362364]
	5	Alonzo Church, The Calculi of Lambda Conversion. (AM-6) (Annals of Mathematics Studies), Princeton University Press, Princeton, NJ, 1985
	6	Curry, H. B., and Feys, R., Combinatory Logic, Vol. I. North-Holland, Amsterdam, 1958
	7	Landin, P. J., A Lambda-Calculus Approach. Advances in Programming and Non-Numerical Computation, Pergamon Press, 1966, 97-141
	8	Floyd, R. W., Assigning Meaning to Programs. Proc. Sym. Applied Math. 19, Amer. Math. Soc. 1967, 19-32
	9	Manna, Z., The Correctness of Programs. J. Computer System Sci. 3 (May 1969), 119-127
	10	C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
	11	Scott, D., Outline of a Mathematical Theory of Computation, Proc. Fourth Annual Princeton Conf. on Information Sciences and Systems (1970), 169-176
	11.1	Scott, D. Lattice Theory, Data Types, and Semantics. New York University Symposia in Areas of Current Interest in Computer Science, ed. R. Randell (1971).
	11.2	Scott, D. Lattice-theoretic Models for Various Type-free Calculi. Proc. Fourth International Congress for Logic, Methodology, and the Philosophy of Science, Bucharest (1972)
	11.3	Scott, D. Continuous Lattices. Proc. 1971 Dalhousie Conf., Springer Lecture Note Series, Springer-Verlag, Heidelburg
	12	Burstall, R. M., Formal Description of Program Structure and Semantics in First Order Logic. Machine Intelligence 5, ed. B. Meltzer and D. Michie, Edinburgh University Press, (1969) 79-98
	13	Lucas, P., Lauer, P., and Stigleitner, H., Method and Notation for Formal Definition of Programming Languages TR 25.087, IBM Laboratory, Vienna, June 1968
	14	Reynolds, J. C., GEDANKEN - A Simple Typeless Language Which Permits Functional Data Structures and Coroutines. ANL-7621, Argonne National Laboratory, Argonne, Ill. September 1969
	15	Morris, L., The Next 700 Programming Language Descriptions. Unpublished
	16	Park, D., Fixpoint Induction and Proofs of Program Properties. Machine Intelligence 5, ed. B. Meltzer and D. Michie, Edinburgh University Press (1969), 59-78
	17	Jerome Feldman , David Gries, Translator writing systems, Communications of the ACM, v.11 n.2, p.77-113, Feb. 1968 [doi>10.1145/362896.362902]
	18	McCarthy, J., Towards a Mathematical Science of Computation. Proc. IFIP Congress 1962, 21-28
	19	Van Wijngaarden, A., Recursive Definition of Syntax and Semantics. Formal Language Description Languages for Computer Programming, ed. T. B. Steel, North-Holland, 1966, 13-24
	20	James H. Morris, Jr., A bonus from van Wijngaarden's device, Communications of the ACM, v.15 n.8, p.773, Aug. 1972 [doi>10.1145/361532.361558]
	21	Michael J. Fischer, Lambda calculus schemata, Proceedings of ACM conference on Proving assertions about programs, p.104-109, January 06-07, 1972, Las Cruces, New Mexico, United States
	22	P. J. Landin, Correspondence between ALGOL 60 and Church's Lambda-notation: part I, Communications of the ACM, v.8 n.2, p.89-101, Feb. 1965 [doi>10.1145/363744.363749]
	23	A. van Wijngaarden, Report on the algorithmic language ALGOL 68, Printing by the Mathematisch Centrum, 1969
	24	Robin Milner, Implementation and applications of Scott's logic for computable functions, Proceedings of ACM conference on Proving assertions about programs, p.1-6, January 06-07, 1972, Las Cruces, New Mexico, United States
	25	Wozencraft, J. M., and Evans, A., Notes on Programming Linguistics, M. I. T., Cambridge, Mass., February 1971
	26	Barron, D. W., Buxton, J. N., Hartley, D. F., Nixon, E., and Strachey, C., The Main Features of CPL. Comput. J. 6 (July 1963), 134-143
	27	Cheatham, T. E., Fischer, A., and Jorrand, P. On the Basis for ELF - An Extensible Language Facility. Proc. AFIPS 1968 FJCC 33, pt. 2, MDI Publications, Wayne, Pa., 937-948
	28	deBakker, J. W., Semantics of Programming Languages. Advances in Information Systems Science 2, ed. J. T. Tou, Plenum Press, New York, 1969