Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching
summary
Presents Total Outcome Logic, a single logic that models program runs as maps from states to semiring-weighted outcomes and adds an explicit divergence outcome so termination and nontermination are first-class. Claims: one metatheory now subsumes partial correctness, incorrectness, total correctness and nontermination proofs across nondeterministic and probabilistic branching. Builds formulas lifted to distributions (waiting functions), an outcome conjunction and divergence primitive, and demonstrates the approach handles examples including unbounded nondeterminism caveats.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:29Outcome Logic’s vision
- 3:16Branching and non-termination
- 6:47Non-termination in waiting functions
- 9:47Programs as waiting functions
- 10:28Assertion language
- 15:06Correctness and incorrectness
- 15:53Modal operators in Total Outcome Logic
- 18:04Program logics summary
related talks
21mOutcome Separation Logic: Local Reasoning for Correctness and Incorrectness with(…)
41mTotal Functions for Automated Reasoning:Building Terminating Theorem Provers
05mNew foundations for probabilistic separation logic
19mHeterogeneous Dynamic Logic: Provability Modulo Program Theories
56mOmnisemantics: Smooth Handling of Nondeterminism (Invited talk)
29mLogical Relations for Effect Capabilities
14mAdequacy for Algebraic Effects Revisited
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties