Textbook on formal syntax (and semantics) of programming languages
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.