The formal semantics of programming languages

What Hacker News says

1. devlovstadMay 2025
   The course did not use slides but instead wrote everything on a whiteboard. The lecture notes are not public afaik.

   The lecturer did suggest the following 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)

   Show morethread
2. the_bennoOct 2021
   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) surely some category theory will be useful, but it's not a foundational prereq.

   Show morethread
3. p0llardJul 2020
   This seems pretty good from a brief flick through; the author. Graham Hutton, is pretty well known in the CS community.

   Some other resources for people who find that this piques their interest and that they want to go deeper:

   * Formal Reasoning About Programs ("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.

   Show morethread
4. pascal_cuoqSep 2014
   The definitions of the semantics of both the input language and the output language of CompCert are operational. If you want to prove functional properties of programs written in the input language with respect to CompCert's definition, you will probably have to define Hoare-Floyd-style axiomatic semantics and 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 static analysis” instead of “verification of functional properties”: http://verasco.imag.fr/wiki/Main_Page

   Show morethread
5. peterfireflyAug 2014
   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 Topics in Types and Programming Languages", 2005 -- Chapter 10 is a juicy 128 pages on Hindley-Milner type inference. Good for both theory and implementation tricks. It looks at HM typing as a constraint system where the rules are Just Right so that if you get a solution you get a solution that is "maximally nice". It describes variants that are perhaps not quite as beautiful but which in some ways are "better" (= can statically check more of your code or where the programmer can express him or herself freer).

   If you want to know more about unification, which is how HM type inference and checking is usually/originally stated:

   Franz Baader and Wayne Snyder, "Handbook of Automated Reasoning", 2001 -- chapter 8 is called 'Unification theory'.

   Peter Norvig, "Correcting A[sic] Widespread Error in Unification Algorithms", 1991 -- many published algorithms were subtly wrong.

   Unification is really an example of a term rewriting system:

   Franz Baader and Tobias Nipkow, "Term Rewriting and All That", 1998.

   It is amazing how much there is to say about a 10-line algorithm (Algorithm W) / such a short set of typing rules / such a small constraint system as the HM type system.

   Show morethread
6. nextosMay 2025
   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 interested in theorem proving, that's a much simpler starting point. Theorems in analysis are already pretty hard on their own.

   Show morethread