# Books on programming language semantics

I've been reading Nielson & Nielson's "Semantics with Applications", and I really like the subject. I'd like to have one more book on programming language semantics -- but I really can get only one.

I took a look at the Turbak/Gifford book, but it's too long-winded; I thought Winskel would be fine, but I have no access to it (it's not in our University library, and I'm short on money), and I'm not even sure if it's not dated. Slonneger seems OK, but the practical part makes it somewhat too long, and I'm not very comfortable with his style.

So my question is -- is Winskel a good book? And is it dated?

Also, are there other concise books on the subject?

• added links to publisher pages for all books. might be useful for others seeking to browse. – Suresh Venkat Dec 4 '10 at 23:31
• What kind of semantics are you interested in? Denotational? Operational? An overview? – Ohad Kammar Dec 5 '10 at 2:43
• @Ohad Kammar: I'm interested in both. – Jay Dec 5 '10 at 5:05

It all depends how deep you want to go, and how much you already know. For a beginner Winksel's book is really nice, but yes, it's not introducing you to the state of the art in semantics as it was written about 20 years ago. Nevertheless it's still a good first introduction to the subject. It might also be worthwhile pointing out that T. Nipkow has formalised a substantial chunk of Winskel's book in Isabelle/HOL, see here. So if you want to learn using interactive proof assistants together with understanding the semantics of programming languages, you have a lot of coherent material to draw on.

Other books that are more advanced are:

• Gunter, Semantics of Programming Languages, a more advanced book focussing on denotational semantics, an approach to semantics, which hasn't lived up to expectations. Focusses on purely functional lanugages and ignores concurrency. This is the book that I taught myself semantics from as an undergraduate, and in retrospect I wish I had used Winksel's book instead. Gunter is not an easy read for a beginner.

• Domains and lambda-calculi by Amadio and Curien. Another book coming written more in the domain-theoretic tradition, although it discusses process calculi.

• John Mitchell's books which have already been mentioned above. They are also mostly about sequential computation.

Books like Pierce's TAPL are very nice, but focus narrowly on one aspect of programming languages, namely types, as important as that is. I would not recommend it as a first introduction to the general area of programming languages, but it is mandatory to read for anyone who wants to learn about types.

Truth be told, I think there's currently no up-to-date introductory book on language semantics that reflects the substantial progress the last decade has seen, with its decisive shift away from denotational methods and sequential computation to concurrency (process calculi and game semantics), axiomatics semantics and the use of interactive proof assistants in verification.

Update 22. April 2014: Tobias Nipkow and Gerwin Klein have published a new book

which can be seen as 'Winskel in Isabelle/HOL'. It's an introduction to the semantics of programming languages (primarily operational and axiomatic) but unlike previous pen-and-paper-based approaches, this book expresses all its mathematics in Isabelle/HOL. In other words, it's at the same time a book about theorem proving.

The book is brand new so I have not used for teaching, but it looks really suitable as an introduction that is pitched at a lower level than Software Foundations by Pierce et al.

• Is there a shift away from denotational methods? Seems to me more like the kind of people who previously would use hand-wavy proofs, nowadays are expected to produce formal proofs. As denotational methods still cannot easily model everything we do, and require many more prerequisites, those researchers use more approachable methods such as games, process calculi, proof assistants. I'm not sure whether there is a decline in denotational methods. – Ohad Kammar Dec 5 '10 at 19:59
• Please do not confuse denotational semantics with domain theory. Game semantics can be, and usually is, perfectly denotational, i.e., the meaning of a program is a function of the meanings of its parts. – Andrej Bauer Dec 5 '10 at 23:02
• I've opened a new thread regarding this comment. But even if I'm not sure I agree with your definition, game semantics are denotational in nature. I think I should replace "games" with "operational semantics" in my comment, and include game semantics as possibly another form of denotational semantics research. cstheory.stackexchange.com/questions/3577/… – Ohad Kammar Dec 5 '10 at 23:53
• I'm not convinced there is a shift. See my first comment, in light of Andrej's comment. – Ohad Kammar Dec 6 '10 at 19:04
• Is there a shift? An interesting question. How can we measure a shift? There are so many criteria we could apply, from the relatively concrete ones like amount of resarch grants given to different approaches, to vague ideas like mind-share. Given how involved we, as researchers, as employees, as applicants for grant money, are in the outcome of such a question, it's unlikely that we'd agree on an answer. – Martin Berger Dec 7 '10 at 12:30

• Winskel, The Formal Semantics of Programming Languages, Google Books preview. I don't know anything about this book. It's on the list because the question specifically asks about it's content, which is online, mostly.
• Morgan, Programming from Specification, list of ps files. The subject is refinement, which is the process of starting with high-level non-executable descriptions and systematically morphing then into something executable. Of course, every refinement step must preserve semantics, so it discusses a certain type of semantics too (based on predicate treansformers mostly).
• Harper, Practical Foundations of Programming Languages, pdf of draft. See the comment by Dave Clarke below.
• Remy, Using, Understanding, and Unraveling the OCaml Language, pdf. This is the book from which I learned functional programming (OCaml, more precisely) and I liked it a lot. It presents the semantics of basic language features in a very nice way and in the process presents lambda calculus and type theory on a needs to know' basis.
• Peyton Jones, The Implementation of Functional Programming Languages, djvu. The first chapters describe lambda calculus (and its operational semantics') and how higher level language features are desugared into lambda calculus. In this sense, the paper gives an operational semantics for functional languages.
• Pierce (ed), Advanced Topics in Types and Programming Languages, Google Books preview.
• Slonneger, Syntax and Semantics of Programming Languages, list of pdf files. I looked at this briefly a long time ago and didn't like it much. It's on the list because it's mentioned in the question.
• Brookes, A Semantics for Concurrent Separation Logic, pdf. This is a big article (80 pages), not a book. I included it because it's a fairly recent development that I find interesting.
• that's a lot of links :) – Suresh Venkat Dec 5 '10 at 6:27
• This would be more useful if it had been presented as a list. Anyway, I'd recommend the Harper book: click "might". – Dave Clarke Dec 5 '10 at 10:27
• I agree. Radu, could you list out the books, so we know what we're clicking on ? this would be an excellent resource. – Suresh Venkat Dec 5 '10 at 19:32
• It's a list now. (The first version was posted around 2am, after sleeping about 5h the previous night. :P) – Radu GRIGore Dec 5 '10 at 23:22

I would divide the books on programming language semantics into two classes: those that focus on modelling programming language concepts and those that focus on the foundational aspects of semantics. There is no reason a book can't do both. But, usually, there is only so much you can put into a book, and the authors also have their own predispositions about what is important.

Winskel's book, already mentioned, does a bit of both the aspects. And, it is a good beginner's book. An equally good, perhaps even better, book is the one I started with: Gordon's Denotational description of programming languages. This was my first book on semantics, which I read soon after I finished my undergraduate work. I have to say it gave me a firm grounding in semantics and I never had to wonder how denotational semantics differs from operational semantics or axiomatic semantics etc. This book will remain my all-time favourite on denotational semantics.

Other books that focus on modeling aspects rather than foundational aspects are the following:

• Tennent's Semantics of programming languages, which is a more-or-less uptodate book on the semantics of imperative programming languages. It is easy to read. However, it tends to be abstract in later parts of the book and you might have to struggle to see why things are being done in a particular way.

• Reynolds's Theories of programming languages. Anybody specializing in semantics should definitely read this book. It is after all by Reynolds. (David Schmidt once remarked to me, "even if Reynolds is reading out the morning newspaper to you, you want to listen carefully, because you might learn something important"!) It has good coverage of both the modelling aspects and foundational aspects.

The best books on foundational aspects are Gunter's (which I regard as a graduate text book), and Mitchell's (which is good reference book to have on your bookshelf because it is quite comprehensive).

• It's very nice to have you here, Uday! – Radu GRIGore Mar 6 '12 at 11:38
• I am glad to be here too. This is a very nice resource! – Uday Reddy Mar 6 '12 at 19:31
• How about:Transitions and Trees: An Introduction to Structural Operational Semantics from Hans Hüttel 2010. Seems to have goood reviews but no one mentions it here. – Arturo Hernandez Oct 26 '13 at 22:03
• @Uday: Thanks for the answer. What do "modelling programming language concepts" and "the foundational aspects of semantics" mean? What are their differences and relations? – Tim Sep 10 '14 at 7:08
• @Tim: To give the semantics of a programming language, you need to some form mathematical structures, e.g., sets in the simplest case, but sophisticated structures like domains, categories, coalgebras etc. for issues that sets can't handle. By "foundational aspects," I mean the theory of these more sophisticated structures. In the former case, the focus is on programming languages and, in the latter case, it is on the mathematical foundations. – Uday Reddy Sep 11 '14 at 9:26

I really enjoyed reading Winskel when I was taking the undergrad course on semantics. I can't tell if it's dated, though, since I don't do research in this field. A plus of Winskel is that you can find it translated in other languages than English.

For a further reading, more at a graduate level, I'd suggest John Mitchell's books Foundations for Programming Languages and Concepts in Programming Languages. If you read only the first chapters, I guess they also meet your requirement of conciseness.

You will not find free drafts of these books, so if you have a restricted budget go for the "might" in Radu's answer.

Well, I'm not an expert on the subject, but there are some general pieces of advice I can give.

First, there are some people who have already read the book and provided reviews on it. For instance, for the Winskel book The Formal Semantics of Programming Languages (see [1] and [2]) I found reviews on Amazon.

This book confuses between syntax and semantics since the beginning, like separating the literals from its values. No special notations were used to differentiate them. This is a crucial issue that the author should address in a topic like this. Also, some other notations he used is quite confusing, like showing the premises and conclusions.

The author seemed to assume that you have ALL the necessary prerequisites as he explained the background materials in a first few chapters (i.e. set theory, operational semantics, inductions, inductive definitions) very briefly. The style the author used in introduction is to put two or three paragraphs of texts and put some formulas then give exercises. Which is, for me, quite frustrating...

18/20 people find the review useful. You can seek Amazon (or other sources) to see more reviews.

Second, Amazon offers Types and Programming Languages and Basic Category Theory for Computer Scientists along with this book. On another topic Dave Clarke offers these books as excellent ones on "Type Systems and Programming Language Semantics." Again, I'm not an expert, but those might be useful for you.

• TaPL goes a bit too slow for my taste. It's a good book, but I mentioned this because the person asking seems worried about "long winded" books. – Radu GRIGore Dec 5 '10 at 2:46
• @Radu: Certainly TAPL is slow, but it is a rather good introduction. The Harper book you mentioned in your links goes much quicker and covers a lot more ground, though it has not yet been completed. – Dave Clarke Dec 5 '10 at 10:25
• Take that Amazon review of Winskel's book with a pinch of salt. It's often used as a recommended text in undergraduate semantics courses and possibly attracts disgruntled students. I've read the book and found the introductory chapters more than sufficient. His notation throughout seemed to be completely standard as well. – Dominic Mulligan Dec 7 '10 at 23:09