Brotherston, James; Le, Quang Loc; Desai, Gauri; Oda, Yukihiro; (2025) Cyclic Proofs in Hoare Logic and its Reverse. In: ENTICS: Electronic Notes in Theoretical Informatics and Computer Science. EPI Sciences: Glasgow, UK. (In press).

Text mfps2025-cyclic-hoare.pdf - Published Version Access restricted to UCL open access staff until 7 May 2026. Download (372kB)

Abstract

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.

Download activity - last month

Export as JSONXMLCSV

Download activity - last 12 months

Export as JSONXMLCSV

Downloads by country - last 12 months

Export as JSONXMLCSV

Archive Staff Only

View Item