Contextual Refinement of Higher-Order Concurrent Probabilistic Programs
summary
Claims a new logic, Foxtrot, that proves contextual refinement for higher-order concurrent probabilistic programs and handles higher-order local state; soundness is mechanized in Rocq on top of the Iris framework and used to verify examples like the adversarial von Neumann coin and Sodium’s randombytes_uniform. The model bakes schedulers into probabilistic execution trees, requires a form of the axiom of choice to stitch witnesses, and exposes subtle unsoundness of some presampling-on-the-right rules. first higher-order separation logic mechanized in Rocq and Iris uses axiom of choice
AI-written summary · about
chapters (9)
- 0:00Welcome
- 0:45Two-threads probabilistic puzzle
- 2:34Contextual equivalence and refinement
- 4:43Foxtrot and its innovations
- 7:57Foxtrot's model and reasoning
- 9:46Proving refinement with Foxtrot
- 11:33Foxtrot's semantics and schedulers
- 16:48Conclusion and future work
- 17:51Q&A
related talks
23mProbabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and(…)
01h 00mKeynote Talk: Outcome Logic: a foundational framework for concurrent and probabilistic(…)
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
19mScenario-based Proofs for Concurrent Objects
54mReasoning about Progress of Concurrent Objects
28mDependent Session Protocols in Separation Logic from First Principles