In the theory of programming languages, the use of proof assistants has become mainstream. It is considered good form to provide a formal connection between a language and its semantics.

Currently, the main tools for this are based on either higher order logic, or on type theory. Here we will focus on Coq, the largest system of the latter class. The ALEA Coq library formalizes discrete measure theory using a variant of the Giry monad, as a submonad of the CPS monad: (A → [0, 1]) → [0, 1]. This allows to use Moggi’s monadic meta-language to give an interpretation of a language Rml into type theory. Rml is a functional language with a primitive for probabilistic choice. This formalization was the basis for the Certicrypt system for verifying security protocols. Easycrypt is still based on the same idea. To be precise, the type of the monad M of measures also requires monotonicity, summability and linearity. However, Coq cannot prove this to be a monad, as the equality on distributions is not the intensional equality of Coq. We solve this technical issue by using homotopy type theory. Importantly, this allows us to use synthetic topology to present a theory which also includes continuous data types like [0, 1]. Such data types are relevant, for instance, in machine learning and differential privacy.

We would be interested in other languages for probabilistic programming with continuous data types which have a precise mathematical semantics and would like to discuss how to formalize them (in type theory).

Extended abstract:

Synthetic topology in Homotopy Type Theory for probabilistic programming

Florian Faissole

Bas Spitters