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.

翻译：内在定义解释器（intrinsic definitional interpreters）是一种在类型推导而非抽象语法树上操作的定义解释器，近来被研究作为定义编程语言动态语义的一种有前景的方法论。其关键优势在于类型安全性能够交互式地引导并约束解释器的构造。与类型关系类似，霍尔逻辑（Hoare logic）被广泛用于保证程序正确性。能否实现内在定义解释器以在霍尔逻辑推导上运行？我们通过开发面向（i）基本霍尔逻辑，以及（ii）包含堆（heap）、基于动态帧（dynamic frame）的局部推理、良基函数（well-founded functions）和行为子类型（behavioral subtyping）的现实逻辑的Rocq定义解释器，深入探索了这一问题。我们方法的核心是一种名为入口索引（entry-indexing）的新技术，用于解释全正确性推导和良基函数。据我们所知，我们的第二项开发首次形式化了包含良基函数、行为子类型和全正确性的基于动态帧的霍尔逻辑，并实现了首个具有动态帧的完全机械化霍尔逻辑。