Synthetic topology in Homotopy Type Theory for probabilistic programming

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

• Bas Spitters (Aarhus Universitet)
• Monday 03 July 2017, 11:00-12:00
• Seminar Room 2, Newton Institute.

If you have a question about this talk, please contact INI IT.

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.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 2, Newton Institute
• bld31

Note that ex-directory lists are not shown.