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?
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.