Towards Definitional Interpreters for Hoare Logics
This work provides a novel methodology for defining Hoare logics that ensures type safety and correctness by construction, benefiting programming language researchers and formal verification practitioners.
The authors explore intrinsic definitional interpreters for Hoare logics, developing two in Rocq: one for a basic logic and one for a realistic logic with heaps, dynamic frames, well-founded functions, and behavioral subtyping. They introduce entry-indexing to interpret total-correctness derivations and well-founded functions, producing the first formalization of a dynamic-frame-based Hoare logic with these features.
Intrinsic definitional interpreters, definitional interpreters that operate on typing derivations instead of abstract syntax trees, have recently been studied as a promising methodology for defining dynamic semantics of programming languages. A key benefit is that type safety interactively guides and constrains the interpreter's construction. Analogously to typing relations, Hoare logic is widely used to guarantee program correctness. Can intrinsic definitional interpreters be realized to operate over Hoare-logic derivations? We explore this question in depth by developing definitional interpreters in Rocq for (i) a basic Hoare logic, and (ii) a realistic logic featuring heaps, dynamic-frame-based local reasoning, well-founded functions, and behavioral subtyping. Central to our approach is a novel technique we call entry-indexing, which we use to interpret total-correctness derivations and well-founded functions. Our second development yields, to our knowledge, the first formalization of a dynamic-frame-based Hoare logic with well-founded functions, behavioral subtyping, and total correctness, as well as the first fully mechanized Hoare logic with dynamic frames.