A Taxonomy of Hoare-Like Logics
summary
Classifies Hoare-like logics by giving a lattice of exact implications between transformers built from predicate transformers and a Kleene-algebra variant TopKAT, identifies seven classes of initial states for weakest-pre variants, constructs strongest-post duals, and proves which logics are contrapositives or equivalent. Key formal claims: Lisbon logic admits a new TopKAT equation (novel), total-correctness is inexpressible in this algebra, and many logics collapse under termination assumptions; the taxonomy exposes a concrete asymmetry explained by algebraic equations.
AI-written summary · about
chapters (12)
- 0:00Hoare-like logics taxonomy
- 1:02Predicate transformers for taxonomy
- 3:06Logics via weakest preconditions
- 4:52Strongest postcondition transformers
- 7:18Final states in forward analysis
- 8:40Liberal variants and incorrectness logics
- 10:47Contrapositive relations between logics
- 11:29Symmetry break in clean algebra
- 13:38New logics and clean algebra equations
- 15:02Conditions for logics equivalence
- 16:29Summary and open questions
- 16:50Q&A
related talks
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
16mA Hoare-Logic Style Refinement Types Formalisation
19mHeterogeneous Dynamic Logic: Provability Modulo Program Theories
22mAlgebraic Effects Meet Hoare Logic in Cubical Agda
25mLearning Formulas in Finite Variable Logics
19mType Inference Logics
27mFunctorial Semantics for Partial Theories
16mGradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification