Towards Definitional Interpreters for Hoare Logics

TL;DR

This paper develops definitional interpreters operating on Hoare-logic derivations, introducing a novel entry-indexing technique, and formalizes advanced Hoare logics with mechanization.

Contribution

It introduces a new approach to interpret Hoare-logic derivations using definitional interpreters and presents the first formalization of complex Hoare logics with mechanization.

Findings

Developed definitional interpreters for basic and advanced Hoare logics.

Introduced the entry-indexing technique for interpreting derivations.

First formalization of a dynamic-frame-based Hoare logic with well-founded functions.

Abstract

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.