Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Sat 19 Jan 2019 16:00 - 16:25 at Sala VI - Contributed Talks 4 Chair(s): Robbert Krebbers

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

Displayed time zone: Belfast change