Etienne Marion

A Formalization of the Ionescu-Tulcea Theorem in Mathlib

Schröer et al. [Philipp Schröer et al., 2023] developed a verification infrastructure for rapid prototyping of automated verification techniques for probabilistic programs (PPs), which is based on the quantitative intermediate verification language HeyVL. In a nutshell, users enc...