Semantics

What does it all mean?

Motivation

The semantics of a language assigns a meaning to each utterance (legal program) of the language.

We need to know precisely and unambiguously the meaning of every program we write. Why would you use a programming language for which no one knew what any of the programs did? The study of programming language semantics gives us the tools to formally define, reason about, and verify the behavior of programs.

What’s New?

There aren’t many books about semantics from the 21st century. It feels like all the methods were made 50 years ago. But surely some things have changed? I asked ChatGPT in mid-2024, back when LLMs were much weaker than today, Have there been any advances in the field of programming language semantics (denotational, operational, etc.) in the last 20 years?. It responded:

Over the last 20 years, the field of programming language semantics, which includes denotational, operational, and axiomatic semantics, has seen numerous advances. Here are some key developments and trends:
  1. Domain-Specific Languages (DSLs): The rise of DSLs has prompted advances in the semantics of specialized languages, tailored for specific domains such as data analysis, web development, and scientific computing. Semantic techniques have been adapted to better support these languages.
  2. Probabilistic and Quantum Computing: Advances in probabilistic programming languages have led to new semantic frameworks to handle uncertainty and randomness, with applications in machine learning and AI. The semantics of quantum programming languages have been developed to support quantum computing paradigms, incorporating quantum mechanics principles into programming language theory.
  3. Concurrency and Parallelism: With the increase in multicore and distributed computing, new semantic models have been developed to better understand and reason about concurrent and parallel programs. Techniques such as compositional semantics and process calculi (e.g., the π-calculus) have been refined and extended.
  4. Type Theory and Dependent Types: Advances in type theory, especially the development of dependent type systems, have influenced the semantics of programming languages. Languages like Coq and Agda, which use dependent types, have rigorous semantic foundations that enable formal verification of program properties.
  5. Mechanized Semantics and Proof Assistants: The use of proof assistants (e.g., Coq, Isabelle, HOL) has grown, allowing for the formalization and mechanization of programming language semantics. These tools help in proving properties about languages and verifying the correctness of language implementations.
  6. Game Semantics: Game semantics has provided new insights into the interactive behavior of programs, especially in the context of programming languages with complex control structures and higher-order functions.
  7. Abstract Interpretation: Advances in abstract interpretation have provided powerful techniques for static analysis, helping to infer properties about programs and ensuring their correctness and safety. This has influenced both operational and denotational semantics.
  8. Software Verification and Model Checking: The integration of semantic techniques with software verification and model checking has been a significant trend. Techniques from operational semantics are often used to create models for verification tools.
  9. Language Interoperability: With the increasing need for interoperability between different programming languages, semantic frameworks have been developed to facilitate the translation and integration of programs written in different languages.
  10. Semantics of Scripting Languages: As scripting languages like JavaScript and Python have become more prevalent, there have been efforts to provide formal semantics for these languages to better understand their behavior and guide their development.
These advances reflect the ongoing evolution and broadening of the field, driven by new computational paradigms, the need for rigorous software verification, and the increasing complexity of software systems.

I asked the same question to Claude.ai in mid-2026:

Advances in Programming Language Semantics (2006–2026)

This is a field that's actually had a remarkably productive two decades, contrary to what you might expect from a "mature" area of theoretical CS. A few major threads stand out:

  1. Step-indexed and guarded recursion techniques. The biggest practical advance for operational semantics has been the development of step-indexed models and, more recently, guarded recursion (via the topos of trees, and later Iris's separation logic framework). These solve a longstanding problem: how do you give semantics to languages with general recursive types and higher-order state, where naive denotational constructions run into circularity?
    • Appel and McAllester's original step-indexing (early 2000s) indexes semantic relations by the number of computation steps remaining, breaking circularity by induction on steps.
    • This evolved into Iris (Jung, Krebbers, Birkedal, Dreyer et al., ~2015 onward), a higher-order concurrent separation logic framework with a rich "language of ghost state" that has become a kind of universal substrate for proving correctness of concurrent and higher-order programs. It's been used to verify everything from fine-grained concurrent data structures to compiler correctness.
  2. Synthetic/categorical approaches. Domain theory meets type theory.
    • Synthetic domain theory and guarded type theory (Birkedal, Møgelberg, and others) reframe denotational semantics inside a type theory with a built-in notion of "later," letting you define recursive types and recursive definitions directly via modal operators rather than ad hoc fixpoint machinery.
    • Game semantics matured substantially: fully abstract models were found for increasingly rich languages (general references, control operators, concurrency), and game semantics became a real tool for program equivalence checking and verification (e.g., used in some software model checking).
  3. Quantitative and probabilistic semantics.
    • Probabilistic programming languages drove a lot of new denotational work, since the category of measurable spaces (Meas) doesn't have a good Cartesian closed structure for higher-order probabilistic programs. This was a real open problem until quasi-Borel spaces (Heunen, Kammar, Staton, Yang, ~2017) gave a clean cccc model supporting higher-order functions, recursion, and continuous distributions together.
    • More broadly, metric/quantitative semantics (program distances, differential privacy semantics, sensitivity-tracking type systems) became a major subfield, partly driven by needs in differential privacy and machine learning systems.
  4. Algebraic effects and handlers. This is arguably the single most influential idea to emerge in this period for structuring operational and denotational semantics alike.
    • Plotkin and Power's algebraic approach to effects, combined with Plotkin and Pretnar's effect handlers (~2009 onward), gave a unifying account of exceptions, state, nondeterminism, and I/O as algebraic operations with handlers as generalized "interpreters."
    • This had huge downstream influence: it's now baked into real languages (OCaml 5's effect handlers, Unison, Koka, Eff) and reshaped how denotational semantics treats computational effects via Freer monads / free monads + handlers rather than monad transformers.
  5. Logical relations go "industrial scale". Logical relations (a technique from the 1970s) got massively scaled up:
    • Relational separation logics and step-indexed Kripke logical relations let researchers prove contextual equivalence, noninterference, and secure compilation results for full-scale languages with mutable state, modules, and concurrency — not just toy calculi.
    • This fed directly into secure compilation and compiler verification projects (CompCert's semantic preservation proofs, CakeML, RustBelt's semantic model of Rust's type system using Iris).
  6. Semantics for real, messy languages. A notable shift: rather than only studying clean core calculi, there's been serious work giving rigorous operational/denotational semantics to actual deployed languages:
    • RustBelt (Jung et al.) gave the first formal semantic soundness proof for a language like Rust, modeling ownership/borrowing via step-indexed separation logic.
    • JavaScript, WebAssembly (Wasm has a fully formal, mechanized semantics from day one — unusual for an industrial language), and x86/ARM memory models all got rigorous treatments.
    • Weak memory models (semantics for concurrent programs under relaxed hardware memory orderings) became its own rich area, blending operational semantics with axiomatic/declarative semantics (e.g., the C11/C++11 memory model controversies, the "promising semantics" work by Kang, Hur et al.).
  7. Homotopy Type Theory's denotational angle. Less directly "PL semantics" but adjacent development: HoTT/univalent foundations (2006 onward, Voevodsky and others) gave new denotational interpretations of type theory via simplicial sets/cubical sets, which fed back into giving better semantics for dependent type theories used in proof assistants (Coq, Agda, Lean) — notably cubical type theory as a computational semantics for univalence.

Hopefully that gets you excited on what is coming next.

How do we “do” Semantics?

Where does the meaning of a program, or of any utterance in any language (natural or constructed) come from? How is the meaning assigned?

It appears an inescapable fact that semantics is driven by the underlying structure of the utterances, not to each individual character, and not even to each individual token. It is the arrangement of the characters and tokens that gives a program its particular meaning. The technical term for arrangement is syntax. Generally, semantics is given by mapping syntactic structures to their meaning.

In this introduction, we’ll be looking at ways to assign meaning, using the language Astro, which we saw previously in our notes on Syntax. Semantics is almost always defined from the abstract syntax of a language, not its concrete syntax. So as a refresher, here’s the abstract syntax of Astro:

Abstract Syntax of Astro
$ \begin{array}{lcl} n: \mathsf{Nml} & & \\ i: \mathsf{Ide} & & \\ e: \mathsf{Exp} & = & n \mid i \mid -e \mid e\;o\;e \mid \mathtt{call}\;i\;e^*\\ o: \mathsf{Bop} & = & + \mid - \mid * \mid / \mid \% \mid ** \\ s: \mathsf{Stm} & = & i = e \mid \mathtt{print}\;e\\ p: \mathsf{Pro} & = & \mathtt{program}\;s^+\\ \end{array}$

Semantic definitions will assign meanings to each of these abstract forms. Something along the lines of:

Meanings can be assigned to programs either formally or informally. Informal semantics are usually given in natural language, while formal semantics are given in a mathematical language. Formal semantics is the only way to be precise and unambiguous. But it’s also...hard. We’ll start with informal semantics, then move to formal semantics.

There’s a third way, actually. We can write an interpreter, and decree: “the meaning of a program in this language simply is the output of the interpreter right here.”

Seriously? The Third Way?

It sounds silly, but it has one advantage: the so-called “compiler correctness problem“ and the so-called “interpreter correctness problem” aren’t problems anymore—the interpreter is correct by definition.

Informal Semantic Descriptions

The traditional way to assign meanings to programs is with natural language. These descriptions, to be fair, try to be super precise. Let’s see an example. We’ll attempt an informal semantics of the language Astro. We’ll be systematic, at least, covering each piece of the abstract syntax definition:

  1. A program executes its statements in order, generating a list of output values.
  2. Before the program begins, the following identifiers are bound like so:
    • The identifier π is bound to the number $\pi$.
    • The identifier sqrt is bound to the function that returns the square root of its sole argument, which must evaluate to a number.
    • The identifier sin is bound to to the function that returns the sine of its sole argument, which must evaluate to a number
    • The identifier cos is bound to to the function that returns the cosine of its sole argument, which must evaluate to a number
    • The identifier hypot is bound to to the function of two numeric arguments, $x$ and $y$ that returns $\sqrt{x^2+y^2}$
  3. The identifier π is a read-only identifier. All other identifiers are not read-only; we call them writable.
  4. An assignment statement evaluates its right hand side, an expression, then binds the identifier on its left hand side to this new numeric value; however the identifier must not have been previously assigned to, or if it had been, the identifier must be writable and bound to a number (not a function).
  5. A print statement evaluates its argument, then writes it to standard output.
  6. The unary and binary operator expressions evaluate their operands then do the obvious corresponding mathematical operation.
  7. A call expression evaluates its arguments, then calls the function bound to the identifier with these argument values. If the identifier was unbound or bound to a number (instead of a function), that is an error.
  8. An expression that is an identifier produces the value bound to that identifier, which must have been previously bound to a number (not a function).

🙄 🫩 🥱 😴 😑

Well that that was long-winded and who knows if we even caught everything?

CLASSWORK
In fact, the informal semantics is still imprecise! To get started, what does it be to be “bound”? What is “previously”? What is a number? Let’s try to find more problems. There are quite a few!

And can you imagine doing this for a real language? It would take hundreds and hundreds of pages? Right? Right.

Exercise: Browse the ECMAScript Language Specification. How many pages long is it?
Exercise: Make a list of sources for the semantics of many popular programming languages. To get started, the (informal) semantics of Python is given in the Python Language Reference, and it’s huge.

Even informal semantics for small languages can get pretty wordy and as always, a bit sus at times since it’s hard to know whether everything has been captured. But small languages make a good case study since we capture and formally define the semantics in a small space.

Before we introduce the methods for formal semantics, we need to develop an intuition.

Intuition Behind Formal Semantics

In Astro, programs evaluate to, or mean, the list of numbers they output. For example:

$$ \begin{array}{c} \Big\Downarrow \\ \boxed{ \begin{array}{l} \texttt{x = 5;} \\ \texttt{print(sqrt(x * 13 + 35));} \\ \texttt{print(3);} \\ \texttt{y = 7;} \\ \texttt{x = x + y * 3;} \\ \texttt{print(x / 8);} \\ \end{array} } \\ \Big\Downarrow \\ [10, 3, 3.25] \end{array}$$

But how? Here’s how. Programs begin in the state in which certain identifiers are bound to initial values, and the output is initially empty. Statement execution transitions through various computation states, where each state is a pair consisting of a memory (mapping identifiers to their values) and the output so far. The initial state is $(m_0, [\,])$ where:

$m_0 = (\lambda x. 0)[\texttt{π}\mapsto \pi][\texttt{sqrt}\mapsto (\lambda x.\sqrt{x})][\texttt{sin}\mapsto \textrm{sin}][\texttt{cos}\mapsto \textrm{cos}][\texttt{hypot}\mapsto \lambda (x,y).\sqrt{x^2+y^2}]$

The computation proceeds through each statement in the program as follows:

$$ \begin{array}{c} (m_0, [\,]) \\ \Downarrow \\ \boxed{\texttt{x = 5;}} \\ \Downarrow \\ (m_0[x \mapsto 5],[\,]) \\ \Downarrow \\ \boxed{\texttt{print(sqrt(x * 13 + 35));}} \\ \Downarrow \\ (m_0[x \mapsto 5], [10]) \\ \Downarrow \\ \boxed{\texttt{print(3);}} \\ \Downarrow \\ (m_0[x \mapsto 5], [10, 3]) \\ \Downarrow \\ \boxed{\texttt{y = 7;}} \\ \Downarrow \\ (m_0[x \mapsto 5, y \mapsto 7], [10, 3]) \\ \Downarrow \\ \boxed{\texttt{x = x + y * 3;}} \\ \Downarrow \\ (m_0[x \mapsto 26, y \mapsto 7], [10, 3]) \\ \Downarrow \\ \boxed{\texttt{print(x / 8);}} \\ \Downarrow \\ (m_0[x \mapsto 26, y \mapsto 7], [10, 3, 3.25]) \\ \end{array}$$

Within each statement, individual expressions are evaluated. Expression evaluations consult the current memory to determine the values of identifiers. In the first statement, we evaluate the expression $\texttt{5}$ to get the value $5$, then the statement itself produces a new memory. We write this as:

\begin{prooftree} \AxiomC{} \UnaryInfC{$[\![\texttt{5}]\!],m_0 \Downarrow 5$} \UnaryInfC{$[\![\texttt{x=5}]\!],m_0,[\,] \Downarrow (m_1, [\,])$} \end{prooftree}

Where we’ve let $m_1 = m_0[x \mapsto 5]$ (to save space). For the second statement, there are a few subexpressions to evaluate. We show the computation like this:

\begin{prooftree} \AxiomC{} \UnaryInfC{$[\![\texttt{x}]\!],m_1 \Downarrow 5$} \AxiomC{} \UnaryInfC{$[\![\texttt{13}]\!],m_1 \Downarrow 13$} \BinaryInfC{$[\![\texttt{x*13}]\!],m_1 \Downarrow 65$} \AxiomC{} \UnaryInfC{$[\![\texttt{35}]\!],m_1 \Downarrow 35$} \BinaryInfC{$[\![\texttt{x*13+35}]\!],m_1 \Downarrow 100$} \AxiomC{$m_1(\texttt{sqrt}) = \lambda x.\sqrt{x}$} \BinaryInfC{$[\![\texttt{sqrt(x*13+35)}]\!],m_1 \Downarrow 10$} \UnaryInfC{$[\![\texttt{print(sqrt(x*13+35))}]\!],m_1,[\,] \Downarrow (m_1, [10])$} \end{prooftree}

So if we can specify rules for each expression, statement, and program, we can formally define the semantics of the entire language, at least its runtime behavior. But we’re missing something. Not every program should have a meaning. A program may violate certain rules, such as using a variable before it has been assigned a value, or calling a function with the wrong number of arguments. These potential violations have to be addressed. A semantics is responsible for formally stating what those rules are.

Context

Given the abstract syntax and informal definition of Astro's semantics above, what would you say about this Astro program?

print(x);

The abstract syntax permits it. The program is well-formed and structurally sound, but the contextual constraint requiring all variables to have been previously assigned is violated. So the program is illegal, and we can tell this without running the program. There are many examples of contextual rules that can be violated by structurally sound programs in many popular programming languages, such as:

But are these syntactically illegal or semantically illegal? Try capturing them in a traditional grammar. It’s hard, because these rules are context-sensitive, and such grammars are notoriously difficult to write in the traditional Chomskian sense. A completely new technology is required to capture context sensitivity in the grammar—two such technologies are attribute grammars and two-level grammars. These are really hard to write and read, but it doesn’t stop people from insisting that they should be used, and that all errors detectable before running a program should be considered syntax errors.

So are contextual errors syntax errors or semantic errors?

For the...
Syntax people say...
Semantics people say...
The context-free structure
“The context-free syntax”
Use CFG/EBNF/PEG
“The syntax”
Use CFG/EBNF/PEG
The context-sensitive rules
“The context-sensitive syntax”
Use attribute grammars or two-level grammars
“The static semantics”
Use semantic rules
The execution behavior
“The semantics”
Use semantic rules
“The dynamic semantics”
Use semantic rules

Seriously, the debate can get heated:

Syntax or Semantics Debate

Whatever, your position is, that fact is that there are two conceptual distinctions in play here. One is the compile-time vs. run-time distinction. The other is the syntax vs. semantics distinction. The former is more technically called the distinction of statics vs. dynamics:

Statics

Things we can know about a program before it is run, simply by inspecting the source code.

Dynamics

Things we only know about a program while it is running, such as certain effects on the environment, which may be driven by external inputs unknown before execution.

Now if you are a “context-sensitive syntax” person, you unify (or conflate) the two distinctions. If you are a “static semantics” person, you treat keep the distinctions separate and orthogonal:

Syntax (Structure)Semantics (Meaning)
Statics (before execution)Dynamics (during execution)
What are the structural entities (e.g., declarations, expressions, statements, modules) and how do they fit together, perhaps with punctuation? What are the non-structural rules that define a legal program (e.g., type checks, argument-parameter matching rules, visibility rules, etc.)? What does a program do? What effects do each of the forms of a well-structured, legal program have on the run-time environment?

For this class, we are going to unapologetically adopt the static semantics perspective. We take syntax to mean structure and semantics to mean meaning. Syntax is part of the statics of a language, and semantics appears in both the statics and dynamics.

Statics vs. Dynamics

Though statics and dynamics are very general terms, most beginners hear them first in the context of type systems. You’ll hear folks speak of a statically-typed language as one in which type checking is done prior to program execution and a dynamically typed language as one in which type checking is done during program execution. In reality, most languages do a little of both, but one or the other usually predominates.

Exercise: If you are up for some research, list cases in which Java checks types dynamically and JavaScript checks types statically.

Semantics of Astro

The distinction between contextual rules (static semantics) and run-time behavior (dynamic semantics) is so significant that it makes good engineering sense to define them separately. Let’s see how this is done in Astro.

Static Semantics

The contextual rules (static semantics) of Astro were given above in our section on informal semantics. Basically, standalone identifiers can only be bound to numeric values, expressions can only be used in ways consistent with their types, you cannot access unbound identifiers, and you may not modify immutable variables. The predefined identifiers are immutable and all others are mutable. The information surrounding the types and access controls on each identifier is kept in a context. When we analyze expressions, we determine their type. When we analyze statements, we update the context if necessary. Analyzing a program is a matter of determining whether all the semantic checks have passed.

We’ll present the static semantics here and go over the many details in class:

Static Semantics of Astro
$$ \frac{}{\mathsf{Num}\!:\mathsf{Type}}$$
$$ \frac{n\!:\mathsf{Nat}}{\mathsf{Fun}\;n\!:\mathsf{Type}}$$
$$ \frac{}{\textsf{ro}\!:\textsf{Access}}$$
$$ \frac{}{\textsf{rw}\!:\textsf{Access}}$$
$\Gamma\!: \mathsf{Context} =_{\textrm{def}}\; \mathsf{Map}\;\mathsf{Identifier}\;(\mathsf{Type} \times \mathsf{Access})$
$$\frac{}{ \Gamma \vdash [\![n]\!]\!: \textsf{Num}}$$
$$\frac{\Gamma(i) = (\textsf{Num}, \_)}{ \Gamma \vdash [\![i]\!]\!: \textsf{Num}}$$
$$\frac{\Gamma \vdash e\!: \textsf{Num}}{ \Gamma \vdash [\![-e]\!]\!: \textsf{Num}}$$
$$\frac{\Gamma \vdash e_1\!: \textsf{Num} \quad \Gamma \vdash e_2\!: \textsf{Num}} { \Gamma \vdash [\![e_1\;o\;e_2]\!]\!: \textsf{Num}}$$
$$\frac{\Gamma(f) = (\textsf{Fun}\;n,\,\_) \quad (\Gamma \vdash e_j\!: \textsf{Num})_{j=1}^n} { \Gamma \vdash [\![\texttt{call}\;f\;e_1,\ldots,e_n]\!]\!: \textsf{Num}}$$
$$\frac{ \Gamma(i) = \bot \lor \Gamma(i) = (\textsf{Num}, \textsf{rw}) \quad \Gamma \vdash e\!: \textsf{Num}} {\Gamma \vdash [\![i=e]\!] \Longrightarrow \Gamma}$$
$$\frac{ \Gamma \vdash e\!: \textsf{Num}} {\Gamma \vdash [\![\texttt{print}\;e]\!] \Longrightarrow \Gamma}$$
$$\frac{(\Gamma_{j-1} \vdash s_j \Longrightarrow \Gamma_{j})_{j=1}^n} { \vdash [\![\mathtt{program}\;s_1,\ldots,s_n]\!]\;\textsf{ok}}$$
$\begin{array}{l} \Gamma_{0} = \{ \\ \quad\texttt{π}\!: (\textsf{Num}, \textsf{ro}), \\ \quad\texttt{sqrt}\!: (\textsf{Fun}\,1, \textsf{ro}), \\ \quad\texttt{sin}\!: (\textsf{Fun}\,1, \textsf{ro}), \\ \quad\texttt{cos}\!: (\textsf{Fun}\,1, \textsf{ro}), \\ \quad\texttt{hypot}\!: (\textsf{Fun}\,2, \textsf{ro}) \\ \} \end{array}$

Dynamic Semantics

The dynamic semantics describe how Astro programs are executed. We define the dynamic semantics under the assumption that the static semantics has already been applied, i.e., only statically meaningful programs are to be considered. Therefore, in the dynamic semantics, there are no arity checks and no type checks. We need not worry about using identifiers that have not yet been assigned, nor attempts to use an identifier bound to the wrong value for its context.

Dynamic Semantics of Astro
$\begin{array}{l} m\!: \textsf{Mem} = \textsf{Map}\;\textsf{Ide}\;(\textsf{Num} \;\mid\; \textsf{Num}^*\to \textsf{Num}) \\ o\!: \textsf{Output} = \textsf{Num}^* \\ \\ \Downarrow_{\small P} \;\subseteq \mathsf{Pro} \times \mathsf{Output} \\ \Downarrow_{\small S} \;\subseteq (\mathsf{Stm} \times \mathsf{Mem} \times \mathsf{Output}) \times (\mathsf{Mem} \times \mathsf{Output}) \\ \Downarrow_{\small E} \;\subseteq (\mathsf{Exp} \times \mathsf{Mem}) \times \mathsf{Num} \end{array}$
$$ \frac{}{[\![n]\!],m \Downarrow n} $$
$$ \frac{}{[\![i]\!],m \Downarrow m(i)} $$
$$ \frac{e,m \Downarrow x}{[\![\mathsf{-}\;e]\!],m \Downarrow -x} $$
$$ \frac{e_1,m \Downarrow x \quad e_2,m \Downarrow y} {[\![e_1\;op\;e_2]\!],m \Downarrow op(x,y)} $$
$$ \frac{( e_i,m \Downarrow a_i)_{i=1}^n} {[\![\texttt{call}\;i\;e_1,\ldots,e_n]\!],m \Downarrow m(i)(a_1,\ldots,a_n)} $$
$$ \frac{e,m \Downarrow x} {[\![i=e]\!],m,o \Downarrow (m[i \mapsto x], o)} $$
$$ \frac{e,m \Downarrow x} {[\![\mathtt{print}\;e]\!],m,o \Downarrow (m, o\,\mathtt{+\!+}\,[x])} $$
$$ \frac{(s_i,m_{i-1}, o_{i-1} \Downarrow (m_i,o_i))_{i=1}^n} {[\![\mathtt{program}\;s_1,\ldots,s_n]\!] \Downarrow o_n} $$
$\begin{array}{l} o_0 = [\,] \\ m_0 = \{\texttt{π}\mapsto \pi, \texttt{sqrt}\mapsto (\lambda x.\sqrt{x}), \texttt{sin}\mapsto \textrm{sin}, \texttt{cos}\mapsto \textrm{cos}, \texttt{hypot}\mapsto (\lambda (x,y).\sqrt{x^2+y^2})\} \end{array}$
CLASSWORK
We have much to discuss.

Approaches to Formal Semantics

Back to doing semantics. Let’s think of some ways we could capture the meaning of a program formally. Some things come to mind:

There are others, such as categorical semantics, game semantics, metric semantics, and predicate transformer semantics, which are more specialized and advanced approaches to formal semantics.

In more detail:

ApproachMethodIdeas
OperationalConcrete Operational SemanticsDefine an actual abstract machine to execute the program.
Structural Operational Semantics (Small-step)A set of inference rules that show when each individual step of a computation can take place and what its effect is.
Natural Semantics (Big-step)A set of inference rules that show the effect of executing whole constructs without regard to intermediate computational states.
DenotationalDirect Denotational SemanticsDefine the meaning of each syntactic construct as a mathematical object in terms of its constituent constructs.
Continuation SemanticsDefine the meaning of each syntactic construct, compositionally, as a mathematical object, where meanings are generally transformations modeling the “remainder of the program” (to better handle errors and disruptive control transfers).
AxiomaticHoare LogicA kind of axiomatic semantics (where the meaning is inferred from defining a set of invariant properties for each construct) focusing on proving the correctness of programs.
Algebraic SemanticsDefine the semantics via an algebra.
HybridAction SemanticsDefine meaning in a way that is more familiar to programmers, with actions, data, and yielders.
Exercise: Take a look at Categorical Semantics, Game Semantics, and Predicate Transformer Semantics. What are they about? What kinds of approaches do they take?

The approach we took in the previous sections to define the semantics of Astro was natural semantics, which is a kind of operational semantics. We’ll be taking deeper dives into both Operational Semantics and Denotational Semantics later in the course.

Semantics in Practice

Formal semantics, and formal methods in general (e.g., proofs of correctness) seem to be underused in practice, except in certain life-critical domains. But the benefit of studying formal semantics leads to much more rigorous approaches to software correctness and security, a very good thing indeed.

Applying semantic rules at compile-time is part of what’s known as static analysis. During static analysis we look for outright errors, of course, but we also look for suspect practices that have the potential for errors or security vulnerabilities. This latter part of static analysis is necessarily outside the code of formal semantics, but it is an extremely important pragmatic issue that requires the developer’s full attention. To learn more about this area of static analysis, you can see my notes on the topics in the context of compiler construction, or even better, to get a sense of the massive scale of static semantic rules in languages, browse the following:

Resources

Where are some places to learn about semantics? Wikipedia is a good place to start:

You might prefer this excellent introductory overview article:

There are a few books that cover formal semantics:

Recall Practice

Here are some questions useful for your spaced repetition learning. Many of the answers are not found on this page. Some will have popped up in lecture. Others will require you to do your own research.

  1. What is the difference between syntax and semantics?
    Syntax is the structure; semantics is meaning.
  2. What is generally used as the “input” to a semantic definition?
    The abstract syntax.
  3. What are three approaches to defining a semantics?
    (1) Informally, with natural language, (2) formally, with mathematical language, and (3) by writing an interpreter and decreeing that the meaning of a program is the output of the interpreter when run on that program.
  4. How is semantics typically defined?
    Semantics is typically defined informally, using natural language.
  5. Why do most language definitions provide a formal syntax but not a formal semantics?
    Syntax is normally context free and very easy to mathematically formalize; semantic definitions often feature quite a few ad-hoc constraints and lots of contextual information which is more clunky to formalize.
  6. When a formal semantics is defined, to what are meanings assigned?
    Meanings are assigned to each construct in the abstract syntax.
  7. What are the three most popular approaches to defining a formal semantics?
    Denotational, operational, and axiomatic.
  8. What are denotational semantics, operational semantics, and axiomatic semantics?
    Denotational semantics assigns mathematical objects to each construct; operational semantics simulates the execution of a program on an abstract machine; axiomatic semantics defines the meaning of each construct in terms of a formal logic.
  9. In an operational semantics, relations, not functions, are typically used. Why?
    Relations make it easy to model the behavior of illegal programs: we simply don’t define anything at all for a program in an illegal state to do.
  10. In an operational semantics, how do we typically model states for expressions? For statements?
    Expressions are modeled as a pair of an expression and a memory; statements are modeled as a triple of a statement, a memory, and I/O streams.
  11. What does the rule for evaluating a negation expression look like in an operational semantics?
    $\dfrac{e,m \Downarrow x}{[\![-e]\!],m \Downarrow -x}$
  12. What does the rule for evaluating a negation operator expression look like in an denotational semantics?
    $\mathscr{E}[\![-e]\!]\,m = -\mathscr{E}e\,m$
  13. How are errors modeled in a typical denotational semantics?
    Errors are typically modeled as a special value, $\bot$.
  14. Why is denotational semantics hard?
    The underlying mathematics required to justify techniques like recursion require some pretty arcane knowledge.
  15. What is the debate between what to call the language definition rules that cannot be captured in a context-free formalism?
    Some people call it context-sensitive syntax and others call it static semantics.
  16. What is the difference between static semantics and dynamic semantics?
    Static semantics deals with meaning we can infer and check just by looking at the program itself (i.e., before the program is run, or “at compile time”); Dynamic semantics deals with the meaning of the program in terms of its effects at run time.
  17. What do static analyzers do?
    Static analyzers look for errors and suspect practices in code that could lead to errors or security vulnerabilities.
  18. What are two popular semantic analyzers for Java?
    FindBugs and PMD

Summary

We’ve covered:

  • Where semantics comes from
  • The drawbacks of an informal, even if precise, semantic specification
  • Broad approaches to formal semantics
  • Where to learn about formal semantics
  • The problem of context
  • Semantics in practice