R. D. Tennent
Skip Abstract Section
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.
- ACM {1971}. Proc. ACM Symp. on Data Structures in Programming Languages. SIGPLAN Notices (ACM Newsletter) 6, 2 (1971).]]Google Scholar
- ACM {1972}. Proc. ACM Conf. on Proving Assertions about Programs. SIGPLAN Notices (ACM Newsletter) 7, 1 (1972) ; also SIGACT News (ACM Newsletter) 14 (1972).]]Google Scholar
- ACM {1973}. Conf. Rec. ACM Syrup. on Principles of Programn-ring Languages, Boston, 1973.]]Google Scholar
- ACM {1975}. Conf. Rec. Second ACM Syrup. on Principles of Programming Languages, Palo Alto, Calif.]]Google Scholar
- 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.]]Google Scholar
- de Bakker, J.W. {1971}. Recursive Procedures. Mathematical Center, Amsterdam, 1971.]]Google Scholar
- de Bakker, J.W. {1974}. Least Fixed Points Re-visited. Mathematical Center, Amsterdam, 1974.]]Google Scholar
- Bekic, H. {1969}. Definable operations in general algebras, and the theory of automata and flowcharts (unpublished).]]Google Scholar
- BranquarL P. {1971}. The composition of semantics in Algol 68. Comm. ACM 14, 11 (Nov. 1971), 697-708.]] Google ScholarDigital Library
- Burstall, R.M. {1967}. Semantics of assignment. In Machine Intelligence 2. American Elsevier, New York, pp. 3-20.]]Google Scholar
- Burstall, R.M. {1968}. Writing search functions in functional form. In Machine Intelligence 3. American Elsevier, New York, pp. 373-385.]]Google Scholar
- Cadiou, J.M. {1972}. Recursive definitions of partial functions and their computations. Tech. Rep. CS-266, Computer Sci. Dep., Stanford U., Stanford, Calif.]]Google Scholar
- Cadiou, J., and Levy, J. {1973}. Mechanizable proofs about parallel processes. 14th Annual IEEE Syrup. on Switching Theory and Automata, pp. 34-48.]]Google Scholar
- Church, A. {1941}. The Calculi of Lambda Conversion. Princeton U. Press, Princeton, N.J.]] Google ScholarDigital Library
- Cohen, E.S. {1975}. A semantic model for parallel systems with scheduling. In ACM {1975}, pp. 87-94.]] Google Scholar
- Dijkstra, E.W. {1972}. Notes on structured programming. In Structured Programming. Academic Press, New York, pp. 1-82.]] Google Scholar
- 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.]]Google Scholar
- Egli, H. {1973}. An analysis of Scott's X-calculus models. TR-73-191, Dep. of Computer Sci., Cornell U., Ithaca, N.Y.]]Google Scholar
- Engeler, E., Ed. {1971 }. Syrup. on Semantics of Algorithmic Languages. Springer-Verlag Lecture Notes Series no. 188, Springer-Verlag, Berlin, Heidelberg, New York.]]Google Scholar
- Gordon, M.J.C. {1973}. Models of pure LISP. Experimental Programming Rep. No. 31. School of Artificial Intelligence, U. of Edinburgh, Edinburgh, Scotland.]]Google Scholar
- 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.]]Google ScholarDigital Library
- Hoare, C.A.R., and Wirth, N. {1973}. An axiomatic definition of the programming language PASCAL. Acta Inf. 2 (1973), pp. 335-355.]]Google ScholarDigital Library
- Kahn, G. {1973}. A preliminary theory for parallel programs. Research Rep. 6, IRIA, France.]]Google Scholar
- Kleene, S. {1952}. Introduction to Metamathematics. Van Nostrand, New York.]]Google Scholar
- Knuth, D.E. {1974}. Structured programming with go to statements. Computing Surveys 6, 4 (Dec. 1974), 261-301.]] Google ScholarDigital Library
- Landin, P.J. {1964}. The mechanical evaluation of expressions. Computer J. 6 (1964), 308-320.]]Google ScholarCross Ref
- Landin, P.J. {1966}. The next 700 programming languages. Comm. ACM9, 3 (Mar. 1966), 157-164.]] Google ScholarDigital Library
- Ledgard, H. {1971}. Ten mini-languages, a study of topical issues in programming languages. Computing Surveys 3, 3 (Sept. 1971), 115-146.]] Google ScholarDigital Library
- Ligler, G.T. {1975a}. A mathematical approach to language design. In ACM {1975}, pp. 41-53.]] Google Scholar
- Ligler, G.T. {1975b}. Surface properties of programming language constructs. International Syrup. on Proving and Improving Programs, Arc-et-Senans, France.]]Google Scholar
- McCarthy, J. {1960}. Recursive functions of symbolic expressions and their computation by machine, I. Comm. ACM3, 4 (April 1960), 184-195.]] Google ScholarDigital Library
- 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.]]Google Scholar
- 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.]]Google Scholar
- Meyer, A.R., and Ritchie, D.M. {1967}. The complexity of LOOP programs. Proc. 22nd ACM National Conference, pp. 465--469.]] Google ScholarDigital Library
- 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.]]Google Scholar
- Milner, R. {1972}. Implementation and applications of Scott's logic for computable functions. In ACM {1972}, pp. 1-6.]] Google Scholar
- Milner, R. {1973a}. Models of LCF. Tech. Rep. CS-73-332, Computer Sci. Dep., Stanford U., Stanford, Calif.]] Google ScholarDigital Library
- Milner, R. {1973b}. Processes: a mathematical model of computing agents. Proc. Logic. Colloquium, Bristol, England.]]Google Scholar
- Milner, R., and Weyrauch, R. {1972}. Proving compiler correctness in a mechanized logic. Machine Intelligence 7. Edinburgh U. Press, Edinburgh, Scotland, pp. 55-70.]]Google Scholar
- Morris, F.L. {1970}. The next 700 formal language descriptions. (unpublished).]]Google Scholar
- 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.]]Google Scholar
- Morris, J.H. { 1971 }. Another recursion induction principle. Comm. ACM 14, 5 (May 1971), 351-354.]] Google ScholarDigital Library
- Mosses, P. {1974}. The mathematical semantics of Algol 60. Tech. Mon. PRG-12, Oxford U. Computing Lab., Programming Research Group.]]Google Scholar
- Naur, P., Ed. {1963}. Revised report on the algorithmic language Algol 60. Comm. ACM6, 1 (Jan. 1963), 1-17.]] Google ScholarDigital Library
- Park, D. {1969}. Fixpoint induction and proofs of program properties. Machine Intelligence 5. American Elsevier, New York, pp. 59-78.]]Google Scholar
- Quine, W.V. {1960}. Word and Object. Technology Press, Cambridge, Mass., and Wiley, New York.]]Google Scholar
- Reynolds, J.C. {1969}. GEDANKEN--a simple typeless language which permits functional data structures and coroutines. ANL-7621, Argonne National Labs., Argonne, IlL]]Google Scholar
- Reynolds, J.C. {1970}. GEDANKEN--a simple typeless language based on the principle of completeness and the reference concept. Comm. ACM 13, 5 (May 1970), 308-319.]] Google ScholarDigital Library
- Reynolds, J.C. {1972a}. Definitional interpreters for higher-order programming languages. Proc. 25th ACM National Conf., pp. 717-740.]] Google ScholarDigital Library
- 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.]]Google Scholar
- Reynolds, J.C. {1975}. On the interpretation of Scott's domains. Symposia Mathematica, VoL 15. Academic Press, London pp. 123-135.]]Google Scholar
- Reynolds, J.C. {1974a}. Towards a theory of type structure. Programming Symp. Paris. Springer-Verlag Lecture Notes in Computer Science, Vol. 19. Springer-Verlag, Berlin, Heidelberg, New York, pp. 408-429.]] Google ScholarDigital Library
- Reynolds, J.C. {1974b}. On the relation between direct and continuation semantics. 2nd Colloquium on Automata, Languages, and Programming, Saarbrucken. Springer-Verlag Lecture Notes in Computer Science, Vol. 14, Springer-Verlag, Berlin, Heidelberg, New York.]] Google ScholarDigital Library
- Rustin, R., Ed. {1972}. Formal Semantics of Programming Languages. Courant Computer Science Symposia 2. Prentice- Hall, Englewood Cliffs, N.J.]]Google Scholar
- 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.]]Google Scholar
- 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.]]Google Scholar
- 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.]]Google Scholar
- Scott, D. {1972a}. Mathematical concepts in programming language semantics. AFIPS Conf. Proc., Vol. 40, 1972 SJCC AFIPS Press, Montvale, N.J., pp. 225-234.]]Google Scholar
- Scott, D. {1972b}. Lattice theory, data types, and semantics. In Rustin {1972}, pp. 65-106.]]Google Scholar
- 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.]]Google Scholar
- Scott, D. {1972d}. Data types as lattices. Unpublished lecture notes, Amsterdam.]]Google Scholar
- 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.]]Google Scholar
- Steel, T., Ed. {1966}. Formal Language Description Languages. North-HoUand Pub. Co., Amsterdam.]]Google Scholar
- Strachey, C. {1966}. Towards a formal semantics. In Steel {1966}, pp. 198-218.]]Google Scholar
- Strachey, C. {1967}. Fundamental concepts in programming languages. In Notes for the International Summer School in Computer Programming, Copenhagen (unpublished).]]Google Scholar
- 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.]]Google Scholar
- 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.]]Google Scholar
- Terment, R.D. {1973}. Mathematical semantics and design of programming languages. Ph.D. Th., Dep. of Computer Sci., U. of Toronto.]]Google Scholar
- Vuillemin, J.E. {1973}. Proof techniques for recursive programs. Tech. Rep. CS-73-393, Computer Sci. Dep., Stanford U.]]Google Scholar
- Wadsworth, C.P. {1971}. Semantics and pragmatics of the lambda calculus. Ph.D. Th., Oxford U.]]Google Scholar
- Wadsworth, C.P. {1975}. The relation between lambda-expressions and their denotations (unpublished).]]Google Scholar
Index Terms
- The denotational semantics of programming languages
Index terms have been assigned to the content through auto-classification.
Recommendations
Definitional interpreters for higher-order programming languages
ACM '72: Proceedings of the ACM annual conference - Volume 2Higher-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 ...
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 ...
Mathematical semantics of SNOBOL4
POPL '73: Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languagesThis paper analyzes the semantics of the programming language SNOBOL4, following the mathematical approach proposed by D. Scott and C. Strachey. The study aims at clarifying a rather unusual semantic structure, and at demonstrating that the mathematical ...
Comments