---
title: "The Formal Semantics of Programming Languages: An Introduction"
authors:
  - "Glynn Winskel"
year: 1993
venue: "MIT Press"
arxiv: null
doi: null
source: "https://mitpress.mit.edu/9780262731034/the-formal-semantics-of-programming-languages/"
topics:
  - semantics
  - winskel
  - textbook
  - operational-denotational
seed_rank: 713
seed_batch: "perfects-pl-2026-08-13"
reviewed: "2026-08-13"
pool: "languages"
relevance_score: 10
lineage: programming-language-foundations
cites:
  - title: "A Structural Approach to Operational Semantics"
    url: "https://doi.org/10.1016/j.jlap.2004.05.001"
    year: 1981
    arxiv: null
    doi: "10.1016/j.jlap.2004.05.001"
  - title: "Toward a Mathematical Semantics for Computer Languages"
    url: "https://www.cs.ox.ac.uk/files/3228/PRG06.pdf"
    year: 1971
    arxiv: null
    doi: null
  - title: "An Axiomatic Basis for Computer Programming"
    url: "https://doi.org/10.1145/363235.363259"
    year: 1969
    arxiv: null
    doi: "10.1145/363235.363259"
  - title: "Domains for Denotational Semantics"
    url: "https://doi.org/10.1007/BFb0012801"
    year: 1982
    arxiv: null
    doi: "10.1007/BFb0012801"
see:
  - "658-a-structural-approach-to-operational-semantics"
  - "612-toward-a-mathematical-semantics-for-computer-languages"
  - "592-an-axiomatic-basis-for-computer-programming"
  - "656-domains-for-denotational-semantics"
---

# The Formal Semantics of Programming Languages: An Introduction

## One-sentence takeaway

IMP is given matching operational, denotational, and Hoare-style meanings so a first course can prove the three views agree.

## Why it matters here

When Broadside or the engine needs to write down what a command language *is* — GRID COMMAND, an agent script, a shader IR — Winskel is the course-shaped path from Plotkin SOS and Scott–Strachey domains to a small language you can actually prove things about.

## Key ideas

- A while-language (IMP) is the running example for big-step and small-step operational semantics.
- Domain theory is introduced only as far as needed to interpret recursion and to prove denotational/operational adequacy.
- Hoare logic is developed against the same IMP, so axiomatic reasoning is another view of the same meaning, not a separate subject.
- Later chapters reach higher-order and parallel languages without abandoning the three-style comparison.
- MIT Press Foundations of Computing, 1993 (ISBN 978-0-262-73103-4).

## Caveats

## Links

- MIT Press: https://mitpress.mit.edu/9780262731034/the-formal-semantics-of-programming-languages/