University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Synthetic topology in Homotopy Type Theory for probabilistic programming

Synthetic topology in Homotopy Type Theory for probabilistic programming

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact info@newton.ac.uk.

BPR - Big proof

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. We improve on the formalization by using homotopy type theory which provides e.g. quotients and functional extensionality. Moreover, homotopy type theory 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 indicate how our axioms are justified by  Kleene-Vesley realizability, a standard model for computation with continuous data types. (Joint work with Florian Faissole.)



This talk is part of the Isaac Newton Institute Seminar Series series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity