摘要
We present a HOL formalization of the foundational parts of Dijkstra's classic monograph “A Discipline of Programming≓. While embedding programming language semantics in theorem provers is hardly new, this particular undertaking raises several interesting questions, and perhaps makes an interesting supplement to the monograph. Moreover, the failure of HOL's first order proof tactic to prove one ‘theorem’ indicates a technical error in the book.
摘要译文
我们提出了Dijkstra经典着作“编程学科”的基础部分的HOL形式化。在定理证明书中嵌入编程语言语义并不是什么新东西，这个特定的事业提出了一些有趣的问题，也许是专着的一个有趣的补充。而且，HOL的一阶证明策略证明一个“定理”的失败表明了本书的一个技术性错误。
John Harrison1. Formalizing Dijkstra. Theorem Proving in Higher Order Logics[M].DE: Springer, 1998: 171-188