Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Ch...
summary
Paper defines operational notions of may- and must-termination as optimal and pessimal termination probabilities, and builds step-indexed logical relations that are sound and complete for the induced contextual preorders. May-equivalence indexes over the natural numbers while must-equivalence requires countable ordinals. The termination probabilities provably equal the maximal and minimal probabilities under all schedulers, and the resulting equational theory validates the distributive combination of probabilistic and nondeterministic choice.
AI-written summary · about
chapters (17)
- 0:00Intro
- 0:46Probabilities and nondeterminism in programming
- 2:10Countable nondeterminism
- 3:47Contextual equivalence
- 4:03Combining probabilities and nondeterminism
- 5:44Solution: step-indexed logical relations
- 6:42Contributions
- 7:30Syntax and operational semantics.
- 8:37Probabilistic must termination
- 13:27Type-indexed relations
- 14:50Contextual refinement
- 16:52Relational interpretation of types (the may-case)
- 17:46Biorthogonality
- 19:34Logical refinement
- 20:37Relational interpretation of types (the must-case)
- 21:08Algebraic theory
- 21:40Conclusions
related talks
24mFrom Enhanced Coinduction towards Enhanced Induction
18mQuantitative Bounds on Resource Usage of Probabilistic Programs
24mVerifying Almost-Sure Termination for Randomized Distributed Algorithms
29mAmplifying Contextual Distance in Higher-Order Languages, using the Law of Large Numbers
28mReasoning about Distributed Reconfigurable Systems
18mSureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine(…)
20mModel Checking Distributed Protocols in Must
13mCharacterizing Implementability of Global Protocols with Infinite States and Data