Alex Simpson: Safety, Relative Tightness and the Probabilistic Frame Rule

Note: We meet in 3.06.

Abstract: Probabilistic separation logic offers an approach to reasoning about imperative probabilistic programs in which a separating conjunction is used as a mechanism for expressing independence properties. Crucial to the effectiveness of the formalism is the frame rule, which enables modular reasoning about independent probabilistic state. We explore a semantic formulation of probabilistic separation logic in which the frame rule has the same simple formulation as in separation logic, without further side conditions. This is achieved by building a notion of safety into specifications, using which we establish a crucial property of specifications, called relative tightness, from which the soundness of the frame rule follows.

(Joint work with Janez Ignacij Jereb. To be presented at MFPS 2025.)