《具体语义》一书通过证明助手的媒介介绍了编程语言的语义。它包括两个部分：第二部分是语义及其应用的介绍，它基于一种简单的命令式编程语言。它涵盖以下主题：操作语义，编译器正确性，（安全）类型系统，程序分析，指称语义，Hoare逻辑和抽象解释。
第II部分中的所有材料都在Isabelle中进行了形式化，但大多数内容也可以独立于第I部分阅读。
来自亚马逊的评论：这是一本很棒的书。我发现它为Isabelle / HOL中的定理证明做了一个很棒的教程。我还发现它对函数式编程非常有用。
本书中有一些问题，在线提供部分完整的模板答案。有时困难重重，令人沮丧，但值得付出努力。
本书以最严格的方式涵盖了计算机科学的基本主题，并附有优雅的极简主义示例。