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.
Deeply embedded Hoare logic (Deeply embedded Hoare logic2.pptx) | 2.44MiB |
Abstract (coqpl19-final4.pdf) | 529KiB |
Sat 19 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
16:00 - 17:40: Contributed Talks 4CoqPL at Sala VI Chair(s): Robbert KrebbersDelft University of Technology | |||
16:00 - 16:25 Talk | Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs CoqPL Qinxiang CaoShanghai Jiao Tong University File Attached | ||
16:25 - 16:50 Talk | Teaching Discrete Mathematics to Early Undergraduates with Software Foundations CoqPL File Attached | ||
16:50 - 17:15 Talk | Ltac2: Tactical Warfare CoqPL File Attached | ||
17:15 - 17:40 Talk | Towards a Coq Formalisation of Build Systems CoqPL File Attached |