Synthetic topology in Homotopy Type Theory for probabilistic programming

Duration: 1 hour 4 mins

Share this media item:

Embed this media item:

<iframe width="_width_" height="_height_" src="https://sms.cam.ac.uk/media/2521651/embed" frameborder="0" scrolling="no" allowfullscreen></iframe>

Choose size:

About this item

Available Formats

About this item

Description:	Spitters, B Monday 3rd July 2017 - 11:00 to 12:00


Created:	2017-07-21 09:32
Collection:	Big proof
Publisher:	Isaac Newton Institute
Copyright:	Spitters, B
Language:	eng (English)


Abstract:	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.)

Abstract:

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.)

Available Formats

Format	Quality	Bitrate	Size
MPEG-4 Video	640x360	1.93 Mbits/sec	926.72 MB	View	Download
WebM	640x360	525.55 kbits/sec	246.35 MB	View	Download
iPod Video	480x270	496.36 kbits/sec	232.67 MB	View	Download
MP3	44100 Hz	252.44 kbits/sec	118.34 MB	Listen	Download
Auto *	(Allows browser to choose a format it supports)