The formal semantics of programming languages
by Glynn Winskel · first published 1993
7mentions
5recommended by
7HN commenters
2014–2025first – last mentioned
71% recommend29% neutral
Why HN recommends it
Graduate-level introduction to programming language semantics covering operational, denotational, and axiomatic approaches with proofs; noted for its domain theory chapter. Suits readers building formal foundations.
Summarised by Claude from recommending comments
Affiliate links. As an Amazon Associate I earn from qualifying purchases.
…("FRAP") by Adam Chlipala - available for free here: http://adam.chlipala.net/frap/. Forms the basis for 6.822 at MIT, and comes with an accompanying Coq formalisation (as well as psets in Coq). * The Formal Semantics of Programming Languages: An Introduction by Glynn Winskel.
on “Principles of Programming Languages (1997) [pdf]” ↗Glynn Winskel, "The Formal Semantics of Programming Languages", 1993 -- a bit dated but still quite good. Covers basic semantics/type theory. Benjamin Pierce, "Types and Programming Languages", 2002 -- y'know, just your basic type theory. Benjamin Pierce, "Advanced…
on “Safely Composable Type-Specific Languages [pdf]” ↗…then prove that this definition is equivalent to the operational semantics definition. An informal version of this proof for a toy language already exists in good textbooks (for instance Winskel's The Formal Semantics of Programming Languages). It is just a matter of scaling up to C and scaling down to the formally verified level. I should also point out that there is an ongoing research project that takes the same approach, with “Abstract-interpretation-based…
on “A shallow survey of formal methods for C code” ↗No, I wouldn't say that category theory is a prerequisite for domain theory in general. I'm most familiar with domain theory from Winskel's "Formal Semantics of Programming Languages" (great book, cited as Win93 in the linked PDF), which has a whole chapter on the subject with no reference to category theory. If you get deeper into domain theory (e.g. by working through this book)…
on “Domain Theory (1994) [pdf]” ↗…supplementary material: - Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about systems (2nd ed.). Cambridge University Press 2004. (Mainly chapters 1, 2) - Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction, MIT Press 1993. (Mainly chapters 1, 2, 3, 6, 11) - Benjamin C. Pierce. Types and Programming Languages. MIT Press 2002. (Mainly chapters 5, 8, 9, 11, 12)
on “Propositions as Types (2014) [pdf]” ↗It's nice to see theorem proving gain some momentum in a mainstream mathematics topic such as analysis. In PLT, we already had a flagship book (The Formal Semantics of Programming Languages by Winskel) formally verified (kind of, it's not a 1-to-1 transcription) using Isabelle (http://concrete-semantics.org) back in the mid 2010s, when tools began to be very polished. IMHO, if someone is…
on “A Lean companion to Analysis I” ↗Oh yes. Grad school is all reading. I recall reading these books in their entirety. Security Engineering. Ross Anderson The Formal Semantics of Programming Languages. Glynn Wynskell. Communicating Sequential Processes. Tony Hoare. This book is surprising in its compactness and lucidity. Pi Calculus. Robin Milner. Semantics With Applications. Hanne Riis Nielson…
on “Structure and Interpretation of Computer Programs (1996) [pdf]” ↗