pith. sign in

arxiv: 2605.02963 · v1 · submitted 2026-05-03 · 💻 cs.PL

Towards Definitional Interpreters for Hoare Logics

Ke Sun , Di Wang , Yuyan Bao , Meng Wang , Dan Hao This is my paper

Pith reviewed 2026-05-09 16:25 UTC · model grok-4.3

classification 💻 cs.PL
keywords definitional interpretersHoare logicdynamic framestotal correctnessbehavioral subtypingentry indexingmechanized semantics
0
0 comments X

The pith

Definitional interpreters can operate directly on Hoare-logic derivations instead of program syntax trees.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper asks whether intrinsic definitional interpreters can be realized to work over Hoare-logic derivations in the same way they work over typing derivations. It answers by constructing two interpreters, one for a basic Hoare logic and one for a realistic logic that includes heaps, dynamic-frame local reasoning, well-founded functions, behavioral subtyping, and total correctness. A new technique called entry-indexing is introduced to interpret total-correctness derivations and ensure well-founded recursion. The result is presented as the first full mechanization of a dynamic-frame Hoare logic that combines all these elements.

Core claim

Intrinsic definitional interpreters for Hoare logics are realized by defining the interpreter through recursion over the structure of Hoare derivations rather than abstract syntax. Type safety in the meta-language guides and constrains each step of the interpreter. For the realistic logic, entry-indexing associates indices with derivation entries to support total-correctness assertions and well-founded functions while maintaining behavioral subtyping.

What carries the argument

Entry-indexing, a technique that indexes entries within total-correctness derivations to interpret well-founded functions and guarantee termination of the definitional interpreter.

If this is right

  • The interpreter's definition is guided at each step by the Hoare rules themselves.
  • Dynamic-frame reasoning and behavioral subtyping can coexist in a single mechanized total-correctness logic.
  • Total-correctness proofs for well-founded functions become directly executable through the indexed derivation.
  • The approach unifies the specification of correctness with the definition of program behavior.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Entry-indexing could be adapted to other assertion logics that involve well-founded recursion or termination arguments.
  • This style of interpreter might allow correctness proofs to participate directly in runtime checks or symbolic execution.
  • The method could extend to separation logics for concurrent programs if similar indexing can track ownership transfer.

Load-bearing premise

Hoare logic derivations contain enough structural information to guide and constrain the construction of a definitional interpreter interactively, in the same manner that typing derivations do.

What would settle it

A total-correctness derivation for a recursive function that cannot be interpreted by the entry-indexed interpreter without the interpreter itself failing to terminate or violating type safety in the meta-language.

Figures

Figures reproduced from arXiv: 2605.02963 by Dan Hao, Di Wang, Ke Sun, Meng Wang, Yuyan Bao.

Figure 1
Figure 1. Figure 1: Rules of the Executable Region Logic the definition of F Order, and require Mv similar to Fv. However, unlike DF, where entry states are carried everywhere and used for shallow well-founded constraints, here we must find a way to encode the well-foundedness constraint in deeply embedded assertions. We achieve this by assuming that at each entry, the measure would be evaluated and saved to an auxiliary vari… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper claims that intrinsic definitional interpreters—operating directly on Hoare-logic derivations rather than program syntax—can be realized in Rocq, with type safety guiding construction analogously to typing relations. It develops two interpreters: a basic Hoare logic and a realistic dynamic-frame logic supporting heaps, local reasoning via frames, well-founded functions, behavioral subtyping, and total correctness. The key enabler is a novel entry-indexing technique for handling total-correctness derivations and well-founded recursion. The second development is presented as the first formalization of a dynamic-frame Hoare logic with these features and the first fully mechanized Hoare logic with dynamic frames.

Significance. If the mechanization is correct, the work is significant for extending the intrinsic definitional interpreter methodology from typing to Hoare logics, yielding machine-checked evidence that derivations can interactively constrain interpreter construction. The realistic development stands out as the first mechanized dynamic-frame Hoare logic incorporating well-founded functions, behavioral subtyping, and total correctness; this fills a documented gap in existing formalizations and provides a reusable Rocq artifact for further research in verified semantics and program logics.

minor comments (2)
  1. [Abstract] Abstract: the phrase 'to our knowledge, the first formalization...' would be strengthened by a one-sentence pointer to the related-work section that justifies the novelty claim with respect to prior mechanized Hoare logics.
  2. [Introduction] The description of entry-indexing is central yet introduced only at a high level in the abstract; a short definitional example or diagram in the introduction would improve accessibility without lengthening the paper.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of our work and their recommendation to accept the paper. The referee's summary accurately captures our contributions regarding intrinsic definitional interpreters for Hoare logics in Rocq, including the entry-indexing technique and the realistic dynamic-frame development.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper presents a mechanized formalization in Rocq of definitional interpreters for Hoare logics, including a realistic dynamic-frame logic with well-founded functions, behavioral subtyping, and total correctness. The central claim is realized by explicit construction via the entry-indexing technique, with the Rocq development serving as direct evidence of realizability. No load-bearing steps reduce to self-definition, fitted inputs renamed as predictions, or self-citation chains; the work is self-contained against the proof assistant's foundations and does not invoke external uniqueness theorems or ansatzes from prior author work to force its results.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on the existence of sound Hoare logic rules that can be interpreted definitionally and on Rocq's ability to encode derivations as data.

axioms (2)
  • domain assumption Hoare logic rules for basic constructs and heaps are sound
    The interpreters are constructed to operate on these rules.
  • standard math Rocq's dependent type theory is consistent
    All mechanized developments rely on this foundation.
invented entities (1)
  • entry-indexing no independent evidence
    purpose: To interpret total-correctness derivations and well-founded functions
    Novel technique introduced to handle termination in the realistic logic.

pith-pipeline@v0.9.0 · 5484 in / 1344 out tokens · 55640 ms · 2026-05-09T16:25:08.191813+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

39 extracted references · 39 canonical work pages

  1. [1]

    Springer (2016)

    Ahrendt, W., Beckert, B., Bubel, R., H¨ ahnle, R., Schmitt, P.H., Ulbrich, M.: De- ductive software verification-the key book. Springer (2016)

    work page 2016

  2. [2]

    Almeida, J.B., Frade, M.J., Pinto, J.S., De Sousa, S.M.: Rigorous software devel- opment: an introduction to program verification, vol. 1. Springer (2011)

    work page 2011

  3. [3]

    In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

    Amin, N., Rompf, T.: Type soundness proofs with definitional interpreters. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. pp. 666–679 (2017)

    work page 2017

  4. [4]

    In: Workshop on Dependent Types in Programming, Gothenburg (1999)

    Augustsson, L., Carlsson, M.: An exercise in dependent types: A well-typed inter- preter. In: Workshop on Dependent Types in Programming, Gothenburg (1999)

    work page 1999

  5. [5]

    Proceedings of the ACM on Programming Languages2(POPL), 1–34 (2017)

    Bach Poulsen, C., Rouvoet, A., Tolmach, A., Krebbers, R., Visser, E.: Intrinsically- typed definitional interpreters for imperative languages. Proceedings of the ACM on Programming Languages2(POPL), 1–34 (2017)

    work page 2017

  6. [6]

    ACM Transactions on Programming Languages and Systems44(4), 1–136 (2023)

    Banerjee, A., Nagasamudram, R., Naumann, D.A., Nikouei, M.: A relational pro- gram logic with data abstraction and dynamic framing. ACM Transactions on Programming Languages and Systems44(4), 1–136 (2023)

    work page 2023

  7. [7]

    Journal of the ACM (JACM)60(3), 1–73 (2013)

    Banerjee, A., Naumann, D.A.: Local reasoning for global invariants, part ii: Dy- namic boundaries. Journal of the ACM (JACM)60(3), 1–73 (2013)

    work page 2013

  8. [8]

    ACM Transactions on Programming Languages and Systems (TOPLAS)40(2), 1–90 (2018)

    Banerjee, A., Naumann, D.A., Nikouei, M.: A logical analysis of framing for spec- ifications with pure method calls. ACM Transactions on Programming Languages and Systems (TOPLAS)40(2), 1–90 (2018)

    work page 2018

  9. [9]

    In: European Conference on Object-Oriented Program- ming

    Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional logic for local reasoning about global invariants. In: European Conference on Object-Oriented Program- ming. pp. 387–411. Springer (2008)

    work page 2008

  10. [10]

    Journal of the ACM (JACM)60(3), 1–56 (2013)

    Banerjee, A., Naumann, D.A., Rosenberg, S.: Local reasoning for global invariants, part i: Region logic. Journal of the ACM (JACM)60(3), 1–56 (2013)

    work page 2013

  11. [11]

    In: Proceedings of the 17th Workshop on Formal Techniques for Java-like Pro- grams

    Bao, Y., Leavens, G.T., Ernst, G.: Conditional effects in fine-grained region logic. In: Proceedings of the 17th Workshop on Formal Techniques for Java-like Pro- grams. pp. 1–6 (2015)

    work page 2015

  12. [12]

    Formal Aspects of Computing30(3), 381–441 (2018)

    Bao, Y., Leavens, G.T., Ernst, G.: Unifying separation logic and region logic to allow interoperability. Formal Aspects of Computing30(3), 381–441 (2018)

    work page 2018

  13. [13]

    Proceedings of the ACM on Programming Languages 1(ICFP), 1–25 (2017)

    Darais, D., Labich, N., Nguyen, P.C., Van Horn, D.: Abstracting definitional in- terpreters (functional pearl). Proceedings of the ACM on Programming Languages 1(ICFP), 1–25 (2017)

    work page 2017

  14. [14]

    In: Dwyer, M.B., Lopes, A

    Darvas, ´A., Leino, K.R.M.: Practical reasoning about invocations and implementa- tions of pure methods. In: Dwyer, M.B., Lopes, A. (eds.) Fundamental Approaches to Software Engineering. pp. 336–351. Springer Berlin Heidelberg, Berlin, Heidel- berg (2007)

    work page 2007

  15. [15]

    In: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of pro- gramming languages

    Ernst, E., Ostermann, K., Cook, W.R.: A virtual class calculus. In: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of pro- gramming languages. pp. 270–282 (2006)

    work page 2006

  16. [16]

    Communications of the ACM12(10), 576–580 (1969)

    Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM12(10), 576–580 (1969)

    work page 1969

  17. [17]

    Twenty- five years of constructive type theory (Venice, 1995)36, 83–111 (1998)

    Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. Twenty- five years of constructive type theory (Venice, 1995)36, 83–111 (1998)

    work page 1995

  18. [18]

    In: International Symposium on Formal Methods

    Kassios, I.T.: Dynamic frames: Support for framing, dependencies and sharing without restrictions. In: International Symposium on Formal Methods. pp. 268–

    work page

  19. [19]

    Springer (2006) Towards Intrinsic Definitional Interpreters for Hoare Logics 17

    work page 2006

  20. [20]

    Formal Aspects of Computing23(3), 267–288 (2011)

    Kassios, I.T.: The dynamic frames theory. Formal Aspects of Computing23(3), 267–288 (2011)

    work page 2011

  21. [21]

    Formal Aspects of Computing 11(5), 541–566 (1999)

    Kleymann, T.: Hoare logic and auxiliary variables. Formal Aspects of Computing 11(5), 541–566 (1999)

    work page 1999

  22. [22]

    In: En- gineering Methods and Tools for Software Safety and Security, pp

    Leino, K.R.M.: Specification and verification of object-oriented software. In: En- gineering Methods and Tools for Software Safety and Security, pp. 231–266. IOS Press (2009)

    work page 2009

  23. [23]

    In: International conference on logic for programming artificial intelligence and reasoning

    Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: International conference on logic for programming artificial intelligence and reasoning. pp. 348–370. Springer (2010)

    work page 2010

  24. [24]

    In: Chechik, M., Wirsing, M

    Leino, K.R.M., Middelkoop, R.: Proving consistency of pure methods and model fields. In: Chechik, M., Wirsing, M. (eds.) Fundamental Approaches to Software Engineering. pp. 231–245. Springer Berlin Heidelberg, Berlin, Heidelberg (2009)

    work page 2009

  25. [25]

    In: Proceedings of the 15th Symposium on Principles and Practice of Declarative Pro- gramming

    Midtgaard, J., Ramsey, N., Larsen, B.: Engineering definitional interpreters. In: Proceedings of the 15th Symposium on Principles and Practice of Declarative Pro- gramming. pp. 121–132 (2013)

    work page 2013

  26. [26]

    Springer (2014)

    Nipkow, T., Klein, G.: Concrete semantics: with Isabelle/HOL. Springer (2014)

    work page 2014

  27. [27]

    In: International Symposium of Formal Meth- ods Europe

    von Oheimb, D., Nipkow, T.: Hoare logic for nanojava: Auxiliary variables, side ef- fects, and virtual methods revisited. In: International Symposium of Formal Meth- ods Europe. pp. 89–105. Springer (2002)

    work page 2002

  28. [28]

    In: European Symposium on Programming

    Owens, S., Myreen, M.O., Kumar, R., Tan, Y.K.: Functional big-step semantics. In: European Symposium on Programming. pp. 589–615. Springer (2016)

    work page 2016

  29. [29]

    The Computer Journal 29(6), 531–537 (01 1986)

    Pandya, P., Joseph, M.: A structure-directed total correctness proof rule for recursive procedure calls. The Computer Journal 29(6), 531–537 (01 1986). https://doi.org/10.1093/comjnl/29.6.531, https://doi.org/10.1093/comjnl/29.6.531

    work page doi:10.1093/comjnl/29.6.531 1986

  30. [30]

    Proceedings of the ACM on Programming Languages6(OOPSLA2), 1903–1932 (2022)

    van der Rest, C., Poulsen, C.B., Rouvoet, A., Visser, E., Mosses, P.: Intrinsically- typed definitional interpreters ` a la carte. Proceedings of the ACM on Programming Languages6(OOPSLA2), 1903–1932 (2022)

    work page 1903

  31. [31]

    In: Proceedings of the ACM annual conference-Volume 2

    Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: Proceedings of the ACM annual conference-Volume 2. pp. 717–740 (1972)

    work page 1972

  32. [32]

    Higher-Order and Symbolic Computation11(4), 355–361 (1998)

    Reynolds, J.C.: Definitional interpreters revisited. Higher-Order and Symbolic Computation11(4), 355–361 (1998)

    work page 1998

  33. [33]

    In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs

    Rouvoet, A., Bach Poulsen, C., Krebbers, R., Visser, E.: Intrinsically-typed defi- nitional interpreters for linear, session-typed languages. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp. 284–298 (2020)

    work page 2020

  34. [34]

    com/2013/05/type-safety-in-three-easy-lemmas.html

    Siek, J.: Type safety in three easy lemmas (2013), http://siek.blogspot. com/2013/05/type-safety-in-three-easy-lemmas.html

    work page 2013

  35. [35]

    Proceedings of the ACM on Programming Languages3(ICFP), 1–29 (2019)

    Sozeau, M., Mangin, C.: Equations reloaded: High-level dependently-typed func- tional programming and proving in coq. Proceedings of the ACM on Programming Languages3(ICFP), 1–29 (2019)

    work page 2019

  36. [36]

    In: 38th European Conference on Object- Oriented Programming (ECOOP 2024)

    Sun, K., Wang, D., Chen, S., Wang, M., Hao, D.: Formalizing, mechanizing, and verifying class-based refinement types. In: 38th European Conference on Object- Oriented Programming (ECOOP 2024). pp. 39–1. Schloss Dagstuhl–Leibniz- Zentrum f¨ ur Informatik (2024)

    work page 2024

  37. [37]

    In: Pro- ceedings of the 2020 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software

    Van Binsbergen, L.T., Verano Merino, M., Jeanjean, P., Van Der Storm, T., Combemale, B., Barais, O.: A principled approach to repl interpreters. In: Pro- ceedings of the 2020 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software. pp. 84–100 (2020) 18 K. Sun et al

    work page 2020

  38. [38]

    ieee access7, 37770–37791 (2019)

    Yang, Z., Lei, H.: Fether: An extensible definitional interpreter for smart-contract verifications in coq. ieee access7, 37770–37791 (2019)

    work page 2019

  39. [39]

    In: Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2

    Yu, P., Wu, N., Donaldson, A.F.: Ratte: Fuzzing for miscompilations in multi- level compilers using composable semantics. In: Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2. pp. 966–981 (2025)

    work page 2025