World Library  
Flag as Inappropriate
Email this Article

Semantics (computer science)

Article Id: WHEBN0000397608
Reproduction Date:

Title: Semantics (computer science)  
Author: World Heritage Encyclopedia
Language: English
Subject: Semantics, Computer accessibility, Abstract data type, Language primitive, Reserved word
Collection: Formal Methods, Formal Specification Languages, Logic in Computer Science, Programming Language Semantics
Publisher: World Heritage Encyclopedia

Semantics (computer science)

In programming language theory, semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages. It does so by evaluating the meaning of syntactically legal strings defined by a specific programming language, showing the computation involved. In such a case that the evaluation would be of syntactically illegal strings, the result would be non-computation. Semantics describes the processes a computer follows when executing a program in that specific language. This can be shown by describing the relationship between the input and output of a program, or an explanation of how the program will execute on a certain platform, hence creating a model of computation.

Formal semantics, for instance, helps to write compilers, better understand what a program is doing and to prove, e.g., that the following if statement

if 1 = 1 then S1 else S2

has the same effect as S1 alone.


  • Overview 1
  • Approaches 2
  • Variations 3
  • Describing relationships 4
  • History 5
  • See also 6
  • References 7
  • Further reading 8
  • External links 9


The field of formal semantics encompasses all of the following:

  • The definition of semantic models
  • The relations between different semantic models
  • The relations between different approaches to meaning
  • The relation between computation and the underlying mathematical structures from fields such as logic, set theory, model theory, category theory, etc.

It has close links with other areas of computer science such as programming language design, type theory, compilers and interpreters, program verification and model checking.


There are many approaches to formal semantics; these belong to three major classes:

  • Denotational semantics, whereby each phrase in the language is interpreted as a denotation, i.e. a conceptual meaning that can be thought of abstractly. Such denotations are often mathematical objects inhabiting a mathematical space, but it is not a requirement that they should be so. As a practical necessity, denotations are described using some form of mathematical notation, which can in turn be formalized as a denotational metalanguage. For example, denotational semantics of functional languages often translate the language into domain theory. Denotational semantic descriptions can also serve as compositional translations from a programming language into the denotational metalanguage and used as a basis for designing compilers.
  • Operational semantics, whereby the execution of the language is described directly (rather than by translation). Operational semantics loosely corresponds to interpretation, although again the "implementation language" of the interpreter is generally a mathematical formalism. Operational semantics may define an abstract machine (such as the SECD machine), and give meaning to phrases by describing the transitions they induce on states of the machine. Alternatively, as with the pure lambda calculus, operational semantics can be defined via syntactic transformations on phrases of the language itself;
  • Axiomatic semantics, whereby one gives meaning to phrases by describing the logical axioms that apply to them. Axiomatic semantics makes no distinction between a phrase's meaning and the logical formulas that describe it; its meaning is exactly what can be proven about it in some logic. The canonical example of axiomatic semantics is Hoare logic.

The distinctions between the three broad classes of approaches can sometimes be vague, but all known approaches to formal semantics use the above techniques, or some combination thereof.

Apart from the choice between denotational, operational, or axiomatic approaches, most variation in formal semantic systems arises from the choice of supporting mathematical formalism.


Some variations of formal semantics include the following:

Describing relationships

For a variety of reasons, one might wish to describe the relationships between different formal semantics. For example:

  • To prove that a particular operational semantics for a language satisfies the logical formulas of an axiomatic semantics for that language. Such a proof demonstrates that it is "sound" to reason about a particular (operational) interpretation strategy using a particular (axiomatic) proof system.
  • To prove that operational semantics over a high-level machine is related by a bisimulation with the semantics over a low-level machine, whereby the low-level abstract machine contains more primitive operations than the high-level abstract machine definition of a given language. Such a proof demonstrates that the low-level machine "faithfully implements" the high-level machine.

It is also possible to relate multiple semantics through abstractions via the theory of abstract interpretation.


Robert W. Floyd is credited with founding the field of programming language semantics in Floyd (1967).[1]

See also


  1. ^ Knuth, Donald E. "Memorial Resolution: Robert W. Floyd (1936-2001)" (PDF). Stanford University Faculty Memorials. Stanford Historical Society. 
  • Floyd, Robert W. (1967). "Assigning Meaning to Programs". In Schwartz, J.T. Mathematical Aspects of Computer Science. Proceedings of Symposium on Applied Mathematics 19. American Mathematical Society. pp. 19–32.  

Further reading

  • Carl Gunter. Semantics of Programming Languages. MIT Press, 1992. (ISBN 0-262-07143-6)
  • Robert Harper. Practical Foundations for Programming Languages. Working draft, 2006. (online, as PDF)
  • Shriram Krishnamurthi. Programming Languages: Application and Interpretation. (online, as PDF)
  • Mitchell, John C.. Foundations for Programming Languages.
  • John C. Reynolds. Theories of Programming Languages. Cambridge University Press, 1998. (ISBN 0-521-59414-6)
  • Kenneth Slonneger and Barry L. Kurtz. Formal Syntax and Semantics of Programming Languages. Addison-Wesley.
  • Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993 (paperback ISBN 0-262-73103-7)
  • Robert D. Tennent (1991). Semantics of Programming Languages. Prentice-Hall.
  • M. Hennessy (1990) The Semantics of Programming Languages: An Elementary Introduction. Wiley.
  • H. Nielson and F. Nielson (1993) Semantics with Applications. A formal Introduction. Wiley.
  • H. Nielson and F. Nielson (2007) Semantics with Applications: An Appetizer. Undergraduate Texts in Computer Science. Springer.
Lecture notes
  • Glynn Winskel. Denotational Semantics. University of Cambridge.

External links

  • Aaby, Anthony (2004). Introduction to Programming Languages.  Semantics.
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.

Copyright © World Library Foundation. All rights reserved. eBooks from Project Gutenberg are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.