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

<compilers>
Theoretical Book on Compilers
CC BY-SA 4.0
2024-03-22T13:11:30.103Z
[Questions asking for off-site resources are discouraged here](https://langdev.meta.stackexchange.com/q/261/89), 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.
kaya3
CC BY-SA 4.0
2024-03-22T15:37:28.407Z
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.
David Young
CC BY-SA 4.0
2024-03-25T09:29:34.770Z
"Term reweiting and all that", Baader, Nipkow can be a good start.
SK-logic
<p>The most classic book that fits that description is probably Glynn Winskel's <em>&quot;The Formal Semantics of Programming Languages: An Introduction&quot;</em>. 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.</p>
<p>I also like Carl A. Gunter's <em>&quot;Semantics of Programming Languages: Structures and Techniques.&quot;</em> 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.</p>
<p>John C. Mitchell's <em>&quot;Foundations for Programming Languages&quot;</em> 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.</p>
<p>Another often recommended book is Benjamin Pierce's <em>&quot;Types and Programming Languages&quot;</em>. 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.</p>
<p>I have some other resource recommendations, including papers, at the very end of <a href="https://langdev.stackexchange.com/a/1954/172">my answer about defining denotational semantics for recursive functions</a>.</p>

CC BY-SA 4.0
2024-03-22T14:56:47.077Z
2024-03-26T17:59:23.820Z
2024-03-26T17:59:23.820Z
David Young
# Theoretical Book on Compilers
Posted by: username_0 on 2024-03-22
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?
**Tags:** compilers
> **Comments:**
> **username_1**: [Questions asking for off-site resources are discouraged here](https://langdev.meta.stackexchange.com/q/261/89), 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.  
> **username_2**: 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.  
> **username_3**: "Term reweiting and all that", Baader, Nipkow can be a good start.  
---
## 1 answers
### Answer by username_2 on 2024-03-22. Score: 7 | Accepted answer
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](https://langdev.stackexchange.com/a/1954/172).
---
