James Brotherston ; Quang Loc Le ; Gauri Desai ; Yukihiro Oda - Cyclic Proofs in Hoare Logic and its Reverse

entics:16696 - Electronic Notes in Theoretical Informatics and Computer Science, December 20, 2025, Volume 5 - Proceedings of MFPS XLI - https://doi.org/10.46298/entics.16696
Cyclic Proofs in Hoare Logic and its ReverseArticle

Authors: James Brotherston ; Quang Loc Le ; Gauri Desai ; Yukihiro Oda

    We examine the relationships between axiomatic and cyclic proof systems for the partial and total versions of Hoare logic and those of its dual, known as reverse Hoare logic (or sometimes incorrectness logic). In the axiomatic proof systems for these logics, the proof rules for looping constructs involve an explicit loop invariant, which in the case of the total versions additionally require a well-founded termination measure. In the cyclic systems, these are replaced by rules that simply unroll the loops, together with a principle allowing the formation of cycles in the proof, subject to a global soundness condition that ensures the well-foundedness of the circular reasoning. Interestingly, the cyclic soundness conditions for partial Hoare logic and its reverse are similar and essentially coinductive in character, while those for the total versions are also similar and essentially inductive. We show that these cyclic systems are sound, by direct argument, and relatively complete, by translation from axiomatic to cyclic proofs.


    Volume: Volume 5 - Proceedings of MFPS XLI
    Published on: December 20, 2025
    Accepted on: October 15, 2025
    Submitted on: April 3, 2025
    Keywords: Logic in Computer Science, Programming Languages