Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs
Many interactive program verification tools are Hoare logic based. Hoare logics and their assertion languages can be formalized by either shallow embedding or deep embedding. The pros and cons of shallowly/deeply embedded formalization for assertion languages have been discussed for long time. But when it comes to the formalization for proof theories, tools like early versions of Verified Software Toolchain (VST), Iris-rust, Charge! etc. all choose shallow embedding to formalize their Hoare logics.
Some useful Hoare logic proof rules are nonderivable from primary rules. At the same time, their soundness proofs can be long and tedious. This talk introduces deeply embedded Hoare logics which solves this problem, avoid long, complex semantic reasoning and proves those rules as meta-properties. We have used this technique in the latest version of VST.
Conference DaySat 19 JanDisplayed time zone: Belfast change
16:00 - 17:40
|Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs|
Qinxiang CaoShanghai Jiao Tong UniversityFile Attached
|Teaching Discrete Mathematics to Early Undergraduates with Software Foundations|
|Ltac2: Tactical Warfare|
|Towards a Coq Formalisation of Build Systems|