I'd like to learn about formal syntax of programming languages: how do we describe the syntax of a programming language and how it should be parsed? How do we assign formal semantics to a parsed program? I've looked at textbooks like this one, but it is very practical. I am looking for something more theoretical: an introduction to specifying programming languages fully formally and assigning a fully formal semantics. Is there such a book?
$\begingroup$
$\endgroup$
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
1
Maybe you will like to book Concrete Semantics (which is freely available as a PDF). It defines the syntax and semantics of an imperative programming language using the proof assistant Isabelle/HOL. In later chapters also types are added to the language and several examples of program analysis are shown.
-
1$\begingroup$ I took a quick look at it, and it's definitely way closer to what I'm looking for! Thanks. $\endgroup$ Commented Jan 18, 2021 at 7:19
$\begingroup$
$\endgroup$
1
The book Practical Foundations for Programming Languages might have what you're looking for.
An older version of the book can be read here.
-
1$\begingroup$ Oh this might be even closer to what I'm looking for, thanks! $\endgroup$ Commented Jan 25, 2021 at 4:44