COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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 programmingAdd 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 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. ## 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
Note that ex-directory lists are not shown. |
## Other listsBody in Mind Centre of International Studies Lecture Series Primary Care## Other talksPolitical Thought, Time and History: An International Conference Development of a Broadly-Neutralising Vaccine against Blood-Stage P. falciparum Malaria Nature's Sovereignty: The Indus Basin and India's Partition Coral reefs and climate change: Ecological surprises from the epicentre of the 2015-2016 El NiĆ±o Investigating the Functional Anatomy of Motion Processing Pathways in the Human Brain TBC |