Keynote Talk: Outcome Logic: a foundational framework for concurrent and probabilistic(…)
summary
Presents Outcome Logic as a concrete framework that gives a compositional denotational semantics for programs mixing nondeterminism/concurrency and randomness, using pom sets with formula for control-flow+concurrency, a convex power set style denotation for nondeterminism/probability, and an outcome conjunction connective to break distributions. Builds a semantics and a program logic: unbounded loops work for the nondeterministic-choice model (POP paper), full concurrent semantics exists but only bounded loops so far, and proofs handle the XOR example where order matters under an adversarial scheduler.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 1:04Motivation for outcome logic
- 5:39Probabilistic concurrent programs
- 10:37Why these programs matter
- 15:35Brittleness of semantics
- 19:47Restricted language with nondeterminism
- 24:02Extending to full concurrency
- 26:12Inspirations from logics
- 36:51Key insights of outcome conjunction
- 40:24Introducing pom sets
- 44:41Probabilistic assertions and rules
- 49:41Proving correctness
- 50:02Conclusion and future directions
- 52:12Q&A
related talks
23mProbabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and(…)
21mContextual Refinement of Higher-Order Concurrent Probabilistic Programs
01h 01mThe Future of Concurrency and Parallelism
24mHigher order programming with probabilistic effects: A model of stochastic memo...
24mA Concurrent Program Logic with a Future and History
54mReasoning about Progress of Concurrent Objects
01h 01mLogic and Probabilistic Circuits 4
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr