Research Seminars @ Illinois

Probability theory tries its best to suppress all details of its measure-theoretic foundation: to the extent possible, random variables and expectations are treated axiomatically without any mention of sample spaces, σ-algebras, or measurability. This presents challenges for programming language semantics and computer formalization, where all details must be made explicit. I will explain how Kripke models, in which Kripke worlds are sample spaces, provide a natural way of tracking such details. Then, I will explain how these Kripke models have a computational reading in which sample spaces form resources akin to pointers and file handles, and how this resourceful perspective informs the design of new logics for probabilistic program verification and new symbolic program analyses.