Verifying Programs with Logic and Extended Proof Rules: Deep Embedding v.s. Shallow Embedding

Zhongye Wang, Qinxiang Cao, Yichen Tao

Many foundational program verification tools have been developed to build machine-checked program correctness proofs, a majority of which are based on Hoare logic. Their program lo…