Skip to main content
SpringerLink
Log in

The Varieties of Programming Language Semantics And Their Uses

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 2001)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2244))

Abstract

Formal descriptions of syntax are quite popular: regular and context-free grammars have become accepted as useful for documenting the syntax of programming languages, as well as for generating efficient parsers; attribute grammars allow parsing to be linked with typechecking and code generation; and regular expressions are extensively used for searching and transforming text. In contrast, formal semantic descriptions are widely regarded as being of interest only to theoreticians. This paper surveys the main frameworks available for describing the dynamic semantics of programming languages. It assesses the potential and actual uses of semantic descriptions, and considers practical aspects, such as comprehensibility, modularity, and extensibility, which are especially significant when describing full-scale languages. It concludes by suggesting that the provision of mature tools for transforming practical semantic descriptions into reasonably efficient compilers and interpreters would significantly increase the popularity of formal semantics.

The paper is intended to be accessible to all computer scientists. Familiarity with the details of particular semantic frameworks is not required, although some understanding of the general concepts of formal semantics is assumed.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Abramsky and G. McCusker. Linearity, sharing, and state: A fully abstract game semantics for Idealized Algol with active expressions (extended abstract). In Proc. 1996 Workshop on Linear Logic, volume 3 of Electronic Notes in TCS. Elsevier, 1996.

    Google Scholar 

  2. L. Aceto, W. Fokkink, and C. Verhoef. Structural operational semantics. In J. A. Bergstra, A. Ponse, and S. A. Smolka, editors, Handbook of Process Algebra, chapter 3, pages 197–291. Elsevier Science, 2001.

    Google Scholar 

  3. C. Alexander. A Timeless Way of Building. Oxford University Press, 1979.

    Google Scholar 

  4. P. America, J. de Bakker, J. N. Kok, and J. J. M. M. Rutten. Denotational semantics of a parallel object-oriented language. Information and Computation, 83(2):152–206, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  5. E. A. Ashcroft, M. Clint, and C. A. R. Hoare. Remarks on ‘Program proving: Jumps and functions, by M. Clint and C. A. R. Hoare’. Acta Inf., 6:317–318, 1976.

    Article  MATH  Google Scholar 

  6. E. Astesiano. Inductive and operational semantics. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts, IFIP State-of-the-Art Report, pages 51–136. Springer-Verlag, 1991.

    Google Scholar 

  7. E. Astesiano and G. Reggio. Smolcs driven concurrent calculi. In TAPSOFT’87, Proc. Int. Joint Conf. on Theory and Practice of Software Development, Pisa, volume 249 of LNCS. Springer-Verlag, 1987.

    Google Scholar 

  8. J. A. Bergstra, J. Heering, and P. Klint, editors. Algebraic Specification. Frontier Series. ACM Press, 1989.

    Google Scholar 

  9. D. Bjørner and C. B. Jones. Formal Specification and Software Development. Prentice-Hall, 1982.

    Google Scholar 

  10. A. Blikle and A. Tarlecki. Naive denotational semantics. In Information Processing 83, Proc. IFIP Congress 83. North-Holland, 1983.

    Google Scholar 

  11. R. Cartwright and M. Felleisen. Extensible denotational semantics specifications. In TACS’94, Proc. Symp. on Theoretical Aspects of Computer Software, Sendai, Japan, volume 789 of LNCS, pages 244–272. Springer-Verlag, 1994.

    Google Scholar 

  12. P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In POPL’92, Proc. 19th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Albuquerque, New Mexico, pages 84–94, 1992.

    Google Scholar 

  13. P. Degano and C. Priami. Enhanced operational semantics. ACM Computing Surveys, 28(2):352–354, June 1996.

    Article  Google Scholar 

  14. A. van Deursen, J. Heering, and P. Klint, editors. Language Prototyping, volume 5 of AMAST Series in Computing. World Scientific, 1996.

    Google Scholar 

  15. E. W. Dijkstra. Guarded commands, non-determinacy, and formal derivations of programs. Commun. ACM, 18:453–457, 1975.

    Article  MATH  MathSciNet  Google Scholar 

  16. M. Felleisen and D. P. Friedman. Control operators, the SECD machine, and the λ-calculus. In Formal Description of Programming Concepts III, Proc. IFIP TC2 Working Conference, Gl. Avernæs, 1986, pages 193–217. North-Holland, 1987.

    Google Scholar 

  17. J. A. Goguen and K. Parsaye-Ghomi. Algebraic denotational semantics using parameterized abstract modules. In J. Diaz and I. Ramos, editors, Proc. Int. Coll. on Formalization of Programming Concepts, Peñiscola, number 107 in LNCS. Springer-Verlag, 1981.

    Google Scholar 

  18. J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Initial algebra semantics and continuous algebras. J. ACM, 24:68–95, 1977.

    Article  MATH  MathSciNet  Google Scholar 

  19. C. A. Gunter and D. S. Scott. Semantic domains. In J. van Leeuwen, A. Meyer, M. Nivat, M. Paterson, and D. Perrin, editors, Handbook of Theoretical Computer Science, volume B, chapter 12. Elsevier Science Publishers, Amsterdam; and MIT Press, 1990.

    Google Scholar 

  20. Y. Gurevich. Evolving algebras 1993: Lipari guide. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1995.

    Google Scholar 

  21. B. S. Hansen and J. Bundgaard. The role of the ANDF formal specification. Technical Report 202104/RPT/5, issue 2, DDC International A/S, Lundtoftevej 1C, DK-2800 Lyngby, Denmark, 1992.

    Google Scholar 

  22. B. S. Hansen and J. U. Toft. The formal specification of ANDF, an application of action semantics. In [42], pages 34–42, 1994.

    Google Scholar 

  23. D. Harel. Dynamic logic. In Handbook of Philosophical Logic, volume II. D. Reidel Publishing Company, 1984.

    Google Scholar 

  24. R. Harper and C. Stone. A type-theoretic interpretation of Standard ML. In G. Plotkin, C. Stirling, and M. Tofte, editors, Robin Milner Festschrifft. MIT Press, 1998.

    Google Scholar 

  25. J. Heering and P. Klint. Semantics of programming languages: A tool-oriented approach. ACM SIGPLAN Notices, Mar. 2000.

    Google Scholar 

  26. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12:576–580, 1969.

    Article  MATH  Google Scholar 

  27. C. A. R. Hoare and H. Jifeng. Unifying Theories of Programming. Prentice-Hall, 1998.

    Google Scholar 

  28. C. A. R. Hoare and P. E. Lauer. Consistent and complementary formal theories of the semantics of programming languages. Act Inf., 3:135–153, 1974.

    MATH  MathSciNet  Google Scholar 

  29. G. Kahn. Natural semantics. In STACS’87, Proc. Symp. on Theoretical Aspects of Computer Science, volume 247 of LNCS, pages 22–39. Springer-Verlag, 1987.

    Google Scholar 

  30. U. Kastens, P. Pfahler, and M. Jung. The eli system. In CC’98, Proceedings 7th International Conference on Compiler Construction, volume 1383 of LNCS, pages 294–297. Springer-Verlag, 1998.

    Google Scholar 

  31. P. J. Landin. A formal description of Algol60. In Formal Language Description Languages for Computer Programming, Proc. IFIP TC2 Working Conference, 1964, pages 266–294. IFIP, North-Holland, 1966.

    Google Scholar 

  32. E. G. Manes and M. A. Arbib. Algebraic Approaches to Program Semantics. Springer-Verlag, 1986.

    Google Scholar 

  33. J. McCarthy. Towards a mathematical science of computation. In Information Processing 62, Proc. IFIP Congress 62, pages 21–28. North-Holland, 1962.

    Google Scholar 

  34. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

    Google Scholar 

  35. R. Milner. Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, A. Meyer, M. Nivat, M. Paterson, and D. Perrin, editors, Handbook of Theoretical Computer Science, volume B, chapter 19. Elsevier Science Publishers, Amsterdam; and MIT Press, 1990.

    Google Scholar 

  36. R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1997.

    Google Scholar 

  37. E. Moggi. An abstract view of programming languages. Technical Report ECSLFCS-90-113, Computer Science Dept., University of Edinburgh, 1990.

    Google Scholar 

  38. E. Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  39. E. Moggi. Metalanguages and applications. In Semantics and Logics of Computation, Publications of the Newton Institute. CUP, 1997.

    Google Scholar 

  40. P. D. Mosses. Denotational semantics. In Handbook of Theoretical Computer Science, volume B, chapter 11. Elsevier Science Publishers, Amsterdam; and MIT Press, 1990.

    Google Scholar 

  41. P. D. Mosses. Action Semantics. Number 26 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

    Google Scholar 

  42. P. D. Mosses, editor. AS’94, Proc. 1st Intl. Workshop on Action Semantics, Edinburgh, number NS-94-1 in Notes Series. BRICS, Dept. of Computer Science, Univ. of Aarhus, 1994. http://www.brics.dk/NS/94/1/BRICS-NS-94-1/.

  43. P. D. Mosses. Foundations of modular SOS. Research Series RS-99-54, BRICS, Dept. of Computer Science, Univ. of Aarhus, 1999. http://www.brics.dk/RS/99/54; full version of [44].

  44. P. D. Mosses. Foundations of Modular SOS (extended abstract). In MFCS’99, volume 1672 of LNCS, pages 70–80. Springer-Verlag, 1999. Full version available at http://www.brics.dk/RS/99/54/.

    Google Scholar 

  45. P. D. Mosses. A modular SOS for Action Notation (extended abstract). In AS’99, number NS-99-3 in Notes Series, pages 131–142, BRICS, Dept. of Computer Science, Univ. of Aarhus, 1999. Full version available athttp://www.brics.dk/RS/99/56/.

  46. P. D. Mosses. A modular SOS for ML concurrency primitives. Research Series RS-99-57, BRICS, Dept. of Computer Science, Univ. of Aarhus, 1999. http://www.brics.dk/RS/99/57/.

  47. P. D. Mosses and D. A. Watt. The use of action semantics. In Formal Description of Programming Concepts III, Proc. IFIP TC2 Working Conference, Gl. Avernæs, 1986, pages 135–166. North-Holland, 1987.

    Google Scholar 

  48. H. R. Nielson and F. Nielson. Semantics with Applications: A Formal Introduction. Wiley, Chichester, UK, 1992.

    MATH  Google Scholar 

  49. F. J. Oles. A Category-Theoretic Approach to the Semantics of Programming Languages. PhD thesis, Syracuse University, 1982.

    Google Scholar 

  50. M. Pettersson. Compiling Natural Semantics, volume 1549 of LNCS. Springer-Verlag, 1999.

    Google Scholar 

  51. G. D. Plotkin. A structural approach to operational semantics. Lecture Notes DAIMI FN-19, Dept. of Computer Science, Univ. of Aarhus, 1981.

    Google Scholar 

  52. J. H. Reppy. CML: A higher-order concurrent language. In Proc. SIGPLAN’91, Conf. on Prog. Lang. Design and Impl., pages 293–305. ACM, 1991.

    Google Scholar 

  53. J. R. X. Ross. An Evaluation Based Approach to Process Calculi. PhD thesis, University of Cambridge, 1999.

    Google Scholar 

  54. D. A. Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn & Bacon, 1986.

    Google Scholar 

  55. D. A. Schmidt. On the need for a popular formal semantics. ACM SIGPLAN Notices, 32(1), 1997.

    Google Scholar 

  56. D. S. Scott and C. Strachey. Toward a mathematical semantics for computer languages. In Proc. Symp. on Computers and Automata, volume 21 of Microwave Research Institute Symposia Series. Polytechnic Institute of Brooklyn, 1971.

    Google Scholar 

  57. R. D. Tennent. The denotational semantics of programming languages. Commun. ACM, 19:437–453, 1976.

    Article  MATH  MathSciNet  Google Scholar 

  58. K. Wansbrough and J. Hamer. A modular monadic action semantics. In Conference on Domain-Specific Languages, pages 157–170. The USENIX Association, 1997.

    Google Scholar 

  59. D. A. Watt. Programming Language Syntax and Semantics. Prentice-Hall, 1991.

    Google Scholar 

  60. D. A. Watt. Why don’t programming language designers use formal methods? In R. Barros, editor, Anais XXIII Seminário Integrado de Software e Hardware, pages 1–16, UFPE, Recife, Brazil, 1996.

    Google Scholar 

  61. P. Wegner. The Vienna definition language. ACM Comput. Surv., 4:5–63, 1972.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. BRICS & Department of Computer Science, University of Aarhus, Ny Munkegade bldg. 540, DK-8000, Aarhus C, Denmark

    Peter D. Mosses

Authors
  1. Peter D. Mosses
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Informatics and Mathematical Modelling, Technical University of Denmark, Bldg.322, 106-108, Richard Petersens Plads, 2800, Lyngby, Denmark

    Dines Bjørner

  2. Computer Science Department, Technical University of Munich, Arcisstr.21, 80290, Munich, Germany

    Manfred Broy

  3. A.P.Ershov Institute of Informatics Systems, Acad.Lavrentjev ave.,6, 630090, Novosibirsk, Russia

    Alexandre V. Zamulin

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mosses, P.D. (2001). The Varieties of Programming Language Semantics And Their Uses. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 2001. Lecture Notes in Computer Science, vol 2244. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45575-2_18

Download citation

  • DOI: https://doi.org/10.1007/3-540-45575-2_18

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43075-9

  • Online ISBN: 978-3-540-45575-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation