Article

Free access

Definitional interpreters for higher-order programming languages

Author:

John C. ReynoldsAuthors Info & Claims

ACM '72: Proceedings of the ACM annual conference - Volume 2

Pages 717 - 740

https://doi.org/10.1145/800194.805852

Published: 01 August 1972 Publication History

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

[1]

McCarthy, J., Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I. Comm ACM 3 (April 1960), 184-195

Digital Library

[2]

Landin, P.J., The Next 700 Programming Languages. Comm ACM 9 (March 1966), 157-166

Digital Library

[3]

Evans, A., PAL - A Language Designed for Teaching Programming Linguistics. Proc. ACM 23rd Natl. Conf., 1968, Brandin Systems Press, Princeton, N. J., 395-403

Digital Library

[4]

Reynolds, J. C., GEDANKEN - A Simple Typeless Language Based on the Principle of Completeness and the Reference Concept. Comm ACM 13 (May 1970), 308-319

Digital Library

[5]

Church, A., The Calculi of Lambda-Conversion. Ann. of Math. Studies 6, Princeton University Press, 1941, 2nd ed. 1951

Digital Library

[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

Digital Library

[10]

Hoare, C. A. R., An Axiomatic Basis for Computer Programming. Comm. ACM 12 (October 1969), 576-580, 583

Digital Library

[11]

Scott, D., Outline of a Mathematical Theory of Computation, Proc. Fourth Annual Princeton Conf. on Information Sciences and Systems (1970), 169-176

[12]

Scott, D. Lattice Theory, Data Types, and Semantics. New York University Symposia in Areas of Current Interest in Computer Science, ed. R. Randell (1971).

[13]

Scott, D. Lattice-theoretic Models for Various Type-free Calculi. Proc. Fourth International Congress for Logic, Methodology, and the Philosophy of Science, Bucharest (1972)

[14]

Scott, D. Continuous Lattices. Proc. 1971 Dalhousie Conf., Springer Lecture Note Series, Springer-Verlag, Heidelburg

[15]

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

[16]

Lucas, P., Lauer, P., and Stigleitner, H., Method and Notation for Formal Definition of Programming Languages TR 25.087, IBM Laboratory, Vienna, June 1968

[17]

Reynolds, J. C., GEDANKEN - A Simple Typeless Language Which Permits Functional Data Structures and Coroutines. ANL-7621, Argonne National Laboratory, Argonne, Ill. September 1969

[18]

Morris, L., The Next 700 Programming Language Descriptions. Unpublished

[19]

Park, D., Fixpoint Induction and Proofs of Program Properties. Machine Intelligence 5, ed. B. Meltzer and D. Michie, Edinburgh University Press (1969), 59-78

[20]

Feldman, J. and Gries, D., Translator Writing Systems. Comm ACM 11 (February 1968), 77-113

Digital Library

[21]

McCarthy, J., Towards a Mathematical Science of Computation. Proc. IFIP Congress 1962, 21-28

[22]

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

[23]

Morris, J. H., A Bonus from Van Wijngaarden's Device. To be published in Comm ACM

Digital Library

[24]

Fischer, M. J., Lambda Calculus Schemata. Proc. ACM Conference on Proving Assertions about Programs, Las Cruces, January 1972, 104-109

Digital Library

[25]

Landin, P. J., A Correspondence Between ALGOL 60 and Church's Lambda-Notation. Comm ACM 8 (February-March 1965), 89-101 and 158-165

Digital Library

[26]

Van Wijngaarden, A., Mailloux, B. J., Peck, J. E. L., and Koster, C. H. A., Report on the Algorithmic Language ALGOL 68. MR 101 Mathematisch Centrum, Amsterdam, October 1969. Also Numerische Mathematik 14 (1969) 79-218

Digital Library

[27]

Milner, R., Implementation and Applications of Scott's Logic for Computable Functions. Proc. ACM Conf. on Proving Assertions about Programs, Las Cruces, January 1972, 1-6

Digital Library

[28]

Wozencraft, J. M., and Evans, A., Notes on Programming Linguistics, M. I. T., Cambridge, Mass., February 1971

[29]

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

[30]

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

[31]

deBakker, J. W., Semantics of Programming Languages. Advances in Information Systems Science 2, ed. J. T. Tou, Plenum Press, New York, 1969

Cited By

Sekiyama TUnno H(2024)Higher-Order Model Checking of Effect-Handling Programs with Answer-Type ModificationProceedings of the ACM on Programming Languages10.1145/36898058:OOPSLA2(2662-2691)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689805
Palmer ZFilardo NWu K(2024)Intensional FunctionsProceedings of the ACM on Programming Languages10.1145/36897148:OOPSLA2(87-112)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689714
Binder DTzschentke MMüller MOstermann K(2024)Grokking the Sequent Calculus (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36746398:ICFP(395-425)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674639
Show More Cited By

Index Terms

Definitional interpreters for higher-order programming languages
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
      1. Interpreters
    2. General programming languages

Recommendations

Definitional Interpreters for Higher-Order Programming Languages

Higher-order programming languages (i.e., languages in which procedures or labels can occur as values) are usually defined by interpreters that are themselves written in a programming language based on the lambda calculus (i.e., an applicative language ...
Definitional Interpreters Revisited

To introduce the republication of “Definitional Interpreters for Higher-Order Programming Languages”, the author recounts the circumstances of its creation, clarifies several obscurities, corrects a few mistakes, and briefly summarizes some more recent ...
The denotational semantics of programming languages

This paper is a tutorial introduction to the theory of programming language semantics developed by D. Scott and C. Strachey. The application of the theory to formal language specification is demonstrated and other applications are surveyed. The first ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ACM '72: Proceedings of the ACM annual conference - Volume 2

August 1972

530 pages

ISBN:9781450374927

DOI:10.1145/800194

Chairman:
John J. Donovan,
Editor:
Rosemary Shields

Copyright © 1972 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

ACM: Association for Computing Machinery

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 August 1972

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

435
Total Citations
View Citations
2,712
Total Downloads

Downloads (Last 12 months)447
Downloads (Last 6 weeks)83

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sekiyama TUnno H(2024)Higher-Order Model Checking of Effect-Handling Programs with Answer-Type ModificationProceedings of the ACM on Programming Languages10.1145/36898058:OOPSLA2(2662-2691)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689805
Palmer ZFilardo NWu K(2024)Intensional FunctionsProceedings of the ACM on Programming Languages10.1145/36897148:OOPSLA2(87-112)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689714
Binder DTzschentke MMüller MOstermann K(2024)Grokking the Sequent Calculus (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36746398:ICFP(395-425)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674639
Zakhour GWeisenburger PSalvaneschi G(2024)Automated Verification of Fundamental Algebraic LawsProceedings of the ACM on Programming Languages10.1145/36564088:PLDI(766-789)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656408
Lorenzen ALeijen DSwierstra WLindley S(2024)The Functional Essence of Imperative Binary Search TreesProceedings of the ACM on Programming Languages10.1145/36563988:PLDI(518-542)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656398
Binder DSkupin ISüberkrüb TOstermann K(2024)Deriving Dependently-Typed OOP from First PrinciplesProceedings of the ACM on Programming Languages10.1145/36498468:OOPSLA1(983-1009)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649846
Ryu SPark J(2024)JavaScript Language Design and Implementation in TandemCommunications of the ACM10.1145/362472367:5(86-95)Online publication date: 1-May-2024
https://dl.acm.org/doi/10.1145/3624723
Foo DSong YChin W(2024)Staged Specification Logic for Verifying Higher-Order Imperative ProgramsFormal Methods10.1007/978-3-031-71162-6_26(501-518)Online publication date: 11-Sep-2024
https://doi.org/10.1007/978-3-031-71162-6_26
Uhlmann YBrunner MBramlage LScheible JCurio C(2023)Procedural- and Reinforcement-Learning-Based Automation Methods for Analog Integrated Circuit Sizing in the Electrical Design SpaceElectronics10.3390/electronics1202030212:2(302)Online publication date: 6-Jan-2023
https://doi.org/10.3390/electronics12020302
Murali APeña LJhala RMadhusudan P(2023)Complete First-Order Reasoning for Properties of Functional ProgramsProceedings of the ACM on Programming Languages10.1145/36228357:OOPSLA2(1063-1092)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622835
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents