7
$\begingroup$

I am looking for books that mostly discuss the theory of compilers (e.g. full-abstraction), and less how to actually build them. Basically, "compilers for mathematicians". Are there any such books, notes or papers?

$\endgroup$
3
  • 2
    $\begingroup$ Questions asking for off-site resources are discouraged here, like they are on Stack Overflow - if there is a question you have about the theory of compilers which might be answered in a book, you can ask that question here directly, though. $\endgroup$
    – kaya3
    Commented Mar 22 at 13:11
  • $\begingroup$ Based on the fact that you ask about full abstraction (which is a certain kind of relationship between a denotational semantics and an operational semantics), I assume you're asking about programming language theory (PLT) rather than compiler theory. Programming language theory is the study of programming languages themselves (largely separate from how they're implemented), while the study of compilers would be more about somewhat lower-level implementation details (how can we build a parser, how can we approach certain kinds of optimizations, etc). I wrote my answer under this assumption. $\endgroup$ Commented Mar 22 at 15:37
  • $\begingroup$ "Term reweiting and all that", Baader, Nipkow can be a good start. $\endgroup$
    – SK-logic
    Commented Mar 25 at 9:29

1 Answer 1

6
$\begingroup$

The most classic book that fits that description is probably Glynn Winskel's "The Formal Semantics of Programming Languages: An Introduction". That covers a lot of the fundamental ideas in programming language theory, including denotational semantics and full abstraction. It also has some material on operational semantics and axiomatic semantics. It starts by talking about operational semantics and has a chapter on how to do induction on the syntax of terms in a programming language as well as induction on derivations, which are important fundamental concepts.

I also like Carl A. Gunter's "Semantics of Programming Languages: Structures and Techniques." This gets right to denotational semantics for lambda calculus. I think it also has a stronger focus on categorical semantics (which is denotational semantics using category theory). From what I've read of it, I've generally found it pretty clearly written. There is some discussion about operational semantics as well.

John C. Mitchell's "Foundations for Programming Languages" is one that I haven't read as much, but it seems very thorough. It's a physically much larger book than the other two books and, appropriately, it seems to go much more in-depth on some topics (for instance, it has an entire chapter on logical relations, which is a useful, though somewhat advanced, topic). It also covers topics the other two don't cover, like Kripke lambda models. I have found it a bit less accessible than the other books, but I also haven't read the foundational chapters in as much detail where he introduces the notation and terminology that he uses later on. The preface also provides a sample outline for a course, with a list of chapters to cover, though I haven't tried following this yet.

Another often recommended book is Benjamin Pierce's "Types and Programming Languages". This is a nice book, but it does not cover denotational semantics (and so there is nothing about full abstraction). It exclusively covers operational semantics. Operational semantics is frequently used for many purposes these days, however.

I have some other resource recommendations, including papers, at the very end of my answer about defining denotational semantics for recursive functions.

$\endgroup$

Not the answer you're looking for? Browse other questions tagged .