The denotational semantics of programming languages

ABSTRACT

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 language considered, LOOP, is very elementary and its definition merely introduces the notation and methodology of the approach. Then the semantic concepts of environments, stores, and continuations are introduced to model classes of programming language features and the underlying mathematical theory of computation due to Scott is motivated and outlined. Finally, the paper presents a formal definition of the language GEDANKEN.

REFERENCES

• 1: ACM {1971}. Proc. ACM Symp. on Data Structures in Programming Languages. SIGPLAN Notices (ACM Newsletter) 6, 2 (1971).
• 2: ACM {1972}. Proc. ACM Conf. on Proving Assertions about Programs. SIGPLAN Notices (ACM Newsletter) 7, 1 (1972) ; also SIGACT News (ACM Newsletter) 14 (1972).
• 3: ACM {1973}. Conf. Rec. ACM Syrup. on Principles of Programn-ring Languages, Boston, 1973.
• 4: ACM {1975}. Conf. Rec. Second ACM Syrup. on Principles of Programming Languages, Palo Alto, Calif.
• 5: Bakker, J.W. {1969}. Semantics of Programming Languages. In Advances in Information Systems Science, Vol. 2, J.T. Tou, Ed., Plenum Press, New York, 1969, pp. 173-227.
• 6: de Bakker, J.W. {1971}. Recursive Procedures. Mathematical Center, Amsterdam, 1971.
• 7: de Bakker, J.W. {1974}. Least Fixed Points Re-visited. Mathematical Center, Amsterdam, 1974.
• 8: Bekic, H. {1969}. Definable operations in general algebras, and the theory of automata and flowcharts (unpublished).
• 9: P. Branquart , J. Lewi , M. Sintzoff , P. L. Wodon, The composition of semantics in Algol 68, Communications of the ACM, v.14 n.11, p.697-708, Nov. 1971 [doi>10.1145/362854.362874]
• 10: Burstall, R.M. {1967}. Semantics of assignment. In Machine Intelligence 2. American Elsevier, New York, pp. 3-20.
• 11: Burstall, R.M. {1968}. Writing search functions in functional form. In Machine Intelligence 3. American Elsevier, New York, pp. 373-385.
• 12: Cadiou, J.M. {1972}. Recursive definitions of partial functions and their computations. Tech. Rep. CS-266, Computer Sci. Dep., Stanford U., Stanford, Calif.
• 13: Cadiou, J., and Levy, J. {1973}. Mechanizable proofs about parallel processes. 14th Annual IEEE Syrup. on Switching Theory and Automata, pp. 34-48.
• 14: Alonzo Church, The Calculi of Lambda Conversion. (AM-6) (Annals of Mathematics Studies), Princeton University Press, Princeton, NJ, 1985
• 15: Ellis S. Cohen, A semantic model for parallel systems with scheduling, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.87-94, January 20-22, 1975, Palo Alto, California [doi>10.1145/512976.512986]
• 16: Dijkstra, E.W. {1972}. Notes on structured programming. In Structured Programming. Academic Press, New York, pp. 1-82.
• 17: Donahue, J.E. {1974}. Mathematical semantics as a complementary definition for defined programming language constructs. Tech. Rep. CSRG-45, Computer Systems Research Group, U. of Toronto, Toronto, Canada.
• 18: Egli, H. {1973}. An analysis of Scott's X-calculus models. TR-73-191, Dep. of Computer Sci., Cornell U., Ithaca, N.Y.
• 19: Engeler, E., Ed. {1971 }. Syrup. on Semantics of Algorithmic Languages. Springer-Verlag Lecture Notes Series no. 188, Springer-Verlag, Berlin, Heidelberg, New York.
• 20: Gordon, M.J.C. {1973}. Models of pure LISP. Experimental Programming Rep. No. 31. School of Artificial Intelligence, U. of Edinburgh, Edinburgh, Scotland.
• 21: Hoare, C.A.R., and Lauer, P.E. {1974}. Consistent and complementary formal theories of the semantics of programming languages. Acta Inf. 3 (1974), pp. 135-153.
• 22: Hoare, C.A.R., and Wirth, N. {1973}. An axiomatic definition of the programming language PASCAL. Acta Inf. 2 (1973), pp. 335-355.
• 23: Kahn, G. {1973}. A preliminary theory for parallel programs. Research Rep. 6, IRIA, France.
• 24: Kleene, S. {1952}. Introduction to Metamathematics. Van Nostrand, New York.
• 25: Donald E. Knuth, Structured Programming with go to Statements, ACM Computing Surveys (CSUR), v.6 n.4, p.261-301, Dec. 1974 [doi>10.1145/356635.356640]
• 26: Landin, P.J. {1964}. The mechanical evaluation of expressions. Computer J. 6 (1964), 308-320.
• 27: 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]
• 28: Henry F. Ledgard, Ten Mini-Languages: A Study of Topical Issues in Programming Languages, ACM Computing Surveys (CSUR), v.3 n.3, p.115-146, Sept. 1971 [doi>10.1145/356589.356592]
• 29: George T. Ligler, A mathematical approach to language design, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.41-53, January 20-22, 1975, Palo Alto, California [doi>10.1145/512976.512982]
• 30: Ligler, G.T. {1975b}. Surface properties of programming language constructs. International Syrup. on Proving and Improving Programs, Arc-et-Senans, France.
• 31: 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]
• 32: McCarthy, J. {1963a}. Towards a mathematical science of computation. In Information Processing 1962. Proc. IFIP Cong. 62. North-Holland Pub. Co., Amsterdam, pp. 21-28.
• 33: McCarthy, J. {1963b}. A basis for a mathematical theory of computation. Computer Programming and Formal Systems, P. Braffort and D. Hirschberg, Eds., North-Holland Pub. Co., Amsterdam, pp. 33-69.
• 34: Albert R. Meyer , Dennis M. Ritchie, The complexity of loop programs, Proceedings of the 1967 22nd national conference, p.465-469, January 1967, Washington, D.C., United States [doi>10.1145/800196.806014]
• 35: Milne, R.E. {1974}. The formal semantics of computer languages and their implementations. Ph.D. Th., Cambridge U. and Tech. Microfiche TCF-2, Oxford U. Computing Lab., Programming Research Group.
• 36: 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
• 37: Robin Milner, Models of LCF., Stanford University, Stanford, CA, 1973
• 38: Milner, R. {1973b}. Processes: a mathematical model of computing agents. Proc. Logic. Colloquium, Bristol, England.
• 39: Milner, R., and Weyrauch, R. {1972}. Proving compiler correctness in a mechanized logic. Machine Intelligence 7. Edinburgh U. Press, Edinburgh, Scotland, pp. 55-70.
• 40: Morris, F.L. {1970}. The next 700 formal language descriptions. (unpublished).
• 41: Morris, F.L. {1972}. Correctness of translations of programming languages, an algebraic approach. Tech. Rep. CS-72-303, Computer Sci. Dep., Stanford U., Stanford, Calif.
• 42: James H. Morris, Jr., Another recursion induction principle, Communications of the ACM, v.14 n.5, p.351-354, May 1971 [doi>10.1145/362588.362598]
• 43: Mosses, P. {1974}. The mathematical semantics of Algol 60. Tech. Mon. PRG-12, Oxford U. Computing Lab., Programming Research Group.
• 44: J. W. Backus , F. L. Bauer , J. Green , C. Katz , J. McCarthy , A. J. Perlis , H. Rutishauser , K. Samelson , B. Vauquois , J. H. Wegstein , A. van Wijngaarden , M. Woodger , P. Naur, Revised report on the algorithm language ALGOL 60, Communications of the ACM, v.6 n.1, p.1-17, Jan. 1963 [doi>10.1145/366193.366201]
• 45: Park, D. {1969}. Fixpoint induction and proofs of program properties. Machine Intelligence 5. American Elsevier, New York, pp. 59-78.
• 46: Quine, W.V. {1960}. Word and Object. Technology Press, Cambridge, Mass., and Wiley, New York.
• 47: Reynolds, J.C. {1969}. GEDANKEN--a simple typeless language which permits functional data structures and coroutines. ANL-7621, Argonne National Labs., Argonne, IlL
• 48: 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]
• 49: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 50: Reynolds, J.C. {1972b}. Notes on a lattice-theoretic approach to the theory of computation. Dep. Systems and Information Science, Syracuse U., Syracuse, New York.
• 51: Reynolds, J.C. {1975}. On the interpretation of Scott's domains. Symposia Mathematica, VoL 15. Academic Press, London pp. 123-135.
• 52: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 53: John C. Reynolds, On the Relation between Direct and Continuation Semantics, Proceedings of the 2nd Colloquium on Automata, Languages and Programming, p.141-156, July 29-August 02, 1974
• 54: Rustin, R., Ed. {1972}. Formal Semantics of Programming Languages. Courant Computer Science Symposia 2. Prentice- Hall, Englewood Cliffs, N.J.
• 55: Scott, D. {1970}. Outline of a mathematical theory of computation. Proc. 4th Princeton Conf. on Information Sciences and Systems; also Tech. Mon. PRG-2, Oxford U. Computing Lab., Programming Research Group, pp. 169-176.
• 56: Scott, D. {1971a}. The lattice of fiow diagrams. In Engeler {1971}; also Tech. Mon. PRG-3, Oxford U. Computing Lab., Programming Research Group, pp. 311-366.
• 57: Scott, D. {1971b}. Continuous lattices. Proc. 1971 Dalhousie Conf. Springer-Verlag Lecture Note Series, No. 274, Springer- Verlag, Berlin, Heidelberg, New York; also Tech. Mort. PRG-7, Oxford U. Computing Lab., Programming Research Group.
• 58: Scott, D. {1972a}. Mathematical concepts in programming language semantics. AFIPS Conf. Proc., Vol. 40, 1972 SJCC AFIPS Press, Montvale, N.J., pp. 225-234.
• 59: Scott, D. {1972b}. Lattice theory, data types, and semantics. In Rustin {1972}, pp. 65-106.
• 60: Scott, D. {I 972c}. Lattice theoretic models for various type-free calculi. Proc. 4th International Cong. for Logic, Methodology, and the Philosophy of Science, Bucharest.
• 61: Scott, D. {1972d}. Data types as lattices. Unpublished lecture notes, Amsterdam.
• 62: Scott, D., and Strachey, C. {1971 }. Towards a mathematical semantics for computer languages. Proc. Symp. on Computers and Automata, Polytechnic Institute of Brooklyn; also Tech. Mon. PRG-6, Oxford U. Computing Lab., pp. 19-46.
• 63: Steel, T., Ed. {1966}. Formal Language Description Languages. North-HoUand Pub. Co., Amsterdam.
• 64: Strachey, C. {1966}. Towards a formal semantics. In Steel {1966}, pp. 198-218.
• 65: Strachey, C. {1967}. Fundamental concepts in programming languages. In Notes for the International Summer School in Computer Programming, Copenhagen (unpublished).
• 66: Strachey, C. {1972}. Varieties of programming language. Proc. International Computing Symp., Cini Foundation, Venice; also Tech. Monograph PRG-10, Oxford U. Computing Lab. Programming Research Group.
• 67: Strachey, C., and Wadsworth, C. {1974}. Continuations, a mathematical semantics for handling full jumps. Tech. Mon. PRG-11. Oxford U. Computing Lab., Programming Research Group.
• 68: Terment, R.D. {1973}. Mathematical semantics and design of programming languages. Ph.D. Th., Dep. of Computer Sci., U. of Toronto.
• 69: Vuillemin, J.E. {1973}. Proof techniques for recursive programs. Tech. Rep. CS-73-393, Computer Sci. Dep., Stanford U.
• 70: Wadsworth, C.P. {1971}. Semantics and pragmatics of the lambda calculus. Ph.D. Th., Oxford U.
• 71: Wadsworth, C.P. {1975}. The relation between lambda-expressions and their denotations (unpublished).

INDEX TERMS

Keywords:
GEDANKEN, LOOP, applicative, continuation, environment, higher-order function, imperative, programming language, recursive definition, semantics, store, theory of computation