Synthetic topology in Homotopy Type Theory for probabilistic programming
1 hour 4 mins,
232.67 MB,
iPod Video
480x270,
29.97 fps,
44100 Hz,
496.36 kbits/sec
Share this media item:
Embed this media item:
Embed this media item:
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.) |
---|
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) |