Fri 20 Jan 2023 10:45 - 11:10 at Avenue34 - Semantics & Effects Chair(s): Stephanie Balzer

Developing denotational models for higher-order languages that combine
probabilistic and nondeterministic choice is known to be very
challenging. In this paper, we propose an alternative approach based
on operational techniques. We study a higher-order language combining
parametric polymorphism, recursive types, discrete probabilistic choice
and countable nondeterminism. We define probabilistic generalizations
of may- and must-termination as the optimal and pessimal probabilities
of termination. Then we define step-indexed logical relations and show
that they are sound and complete with respect to the induced contextual
preorders. For may-equivalence we use step-indexing over the natural
numbers whereas for must-equivalence we index over the countable
ordinals. We then show than the probabilities of may- and
must-termination coincide with the maximal and minimal probabilities of
termination under all schedulers. Finally we derive the equational
theory induced by contextual equivalence and show that it validates the
distributive combination of the algebraic theories for probabilistic
and nondeterministic choice.

Fri 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:45 - 12:00
Semantics & EffectsPOPL at Avenue34
Chair(s): Stephanie Balzer Carnegie Mellon University
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice
Alejandro Aguirre Aarhus University, Lars Birkedal Aarhus University
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
Nicolas Chappe University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Paul He University of Pennsylvania, Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Yannick Zakowski University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Steve Zdancewic University of Pennsylvania
Hefty Algebras: Modular Elaboration of Higher-Order Algebraic EffectsRecorded
Casper Bach Poulsen Delft University of Technology, Cas van der Rest Delft University of Technology
DOI Pre-print