Foundations of denotational semantics

  • Joseph E. Stoy
Constructive Definitions
Part of the Lecture Notes in Computer Science book series (LNCS, volume 86)


Chapters I and II of this paper provide an elementary introduction to the mathematical theory underlying the denotational semantic definition techniques described in this volume; the next two chapters discuss some techniques of use in reasoning about such definitions, and Chapter V describes one way of handling the semantics of languages involving jumps.


Complete Lattice Abstract Syntax Congruence Condition Structural Induction Fixed Point Property 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Burstall, R.M.: Proving Properties of Programs by Structural Induction; Comp. J. 12, 41 (1969).Google Scholar
  2. [2]
    Hoare, C.A.R.: An Axiomatic Basis for Computer Programming; CACM 12, 576 (1969).Google Scholar
  3. [3]
    Jones, C.B.: Denotational Semantics of goto: an Exit Formulation and its Relation to Continuations; p. 278 of: Bjørner, D., and Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language; (Springer-Verlag, 1978).Google Scholar
  4. [4]
    Milne, R.E., and Strachey, C.: A Theory of Programming Language Semantics; (Chapman and Hall, London, and Wiley, New York, 1976).Google Scholar
  5. [5]
    Plotkin, G.D.: A Power Domain Construction; SIAM J. Comp. 5, 452 (1976).CrossRefGoogle Scholar
  6. [6]
    Sanderson, J.G.: The Lambda Calculus, Lattice Theory and Reflexive Domains; Mathematical Institute Lecture Notes, University of Oxford (1973).Google Scholar
  7. [7]
    Scott, D.S.: Outline of a Mathematical Theory of Computation; Proc. Fourth Annual Princeton Conference on Information Sciences and Systems, 169 (Princeton University, 1970); and Technical Monograph PRG-2, Programming Research Group, University of Oxford (1970).Google Scholar
  8. [8]
    Scott, D.S.: Models for Various Type-free Calculi; p. 157 of: Suppes, P., Henkin, L., Joja, A., and Moisil, G.C. (eds.): Logic, Methodology and Philosophy of Science IV; (North-Holland, 1973).Google Scholar
  9. [9]
    Scott, D.S.: Data Types as Lattices; SIAM J. Comp. 5, 522 (1976).CrossRefGoogle Scholar
  10. [10]
    Scott, D.S., and Strachey, C.: Toward a Mathematical Semantics for Computer Languages; p. 19 of: Fox, J. (ed.): Proceedings of the Symposium on Computers and Automata; (Polytechnic Institute of Brooklyn Press, 1971); and Technical Monograph PRG-6, Programming Research Group, University of Oxford (1971).Google Scholar
  11. [11]
    Smyth, M.B.: Powerdomains; Theory of Computation Report 12, Department of Computer Science, University of Warwick (1976).Google Scholar
  12. [12]
    Stoy, J.E.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory; (MIT Press, 1977).Google Scholar
  13. [13]
    Strachey, C., and Wadsworth, C.P.: Continuations: A Mathematical Semantics for Handling Full Jumps; Technical Monograph PRG-11 (Oxford University Computing Laboratory, Programming Research Group, 1974).Google Scholar
  14. [14]
    Tarski, A.: A Lattice-Theoretical Fixpoint Theorem and its Applications; Pacific J. of Maths 5, 285 (1955).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1980

Authors and Affiliations

  • Joseph E. Stoy
    • 1
  1. 1.Programming Research GroupOxford University Computing LaboratoryOxfordEngland

Personalised recommendations