Omnisemantics: Smooth Handling of Nondeterminism (Invited talk)
summary
Defines operational judgments that map a start state to a set of outcomes so one derivation captures every nondeterministic run, formalized in Coq and used throughout a verified stack including Bedrock2. Supports demonic nondeterminism, models undefined behavior by requiring safety for all branches, and equates to a weakest‑precondition style so forward simulations imply backward simulations. Works for big‑ and small‑step, eases compiler proofs and combined progress/preservation, but currently struggles with preserving nontermination/angelic choices.
AI-written summary · about
chapters (6)
- 0:00Start
- 5:08Undefined Behavior & Nondeterminism: Problem 2
- 13:08New* Judgment: Omni-Bigstep Semantics
- 17:31Relationship to Traditional Semantics
- 22:47Omnisemantics Forward Simulation Implies Traditional Backward Simulation
- 47:18Application: Type Safety Proofs
related talks
19mA Pure Demand Operational Semantics with Applications to Program Analysis
49mSemantic Foundations for Probabilistic Programming
14mAdequacy for Algebraic Effects Revisited
18mProbabilistic Kleene Algebra with Angelic Nondeterminism
18mCertified Semantics for Disequality
15mStable Relations and Abstract Interpretation of Higher-Order Programs
15mCompiling with Continuations, Correctly
22mCategorical Semantics of Probabilistic Symbolic Execution