BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Synthetic topology in Homotopy Type Theory for probabilistic progr
 amming - Bas Spitters (Aarhus Universitet)
DTSTART:20170703T100000Z
DTEND:20170703T110000Z
UID:TALK73128@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:The ALEA Coq library formalizes discrete measure theory using 
 a<br>variant of the Giry monad\, as a submonad of the CPS&nbsp\;monad: (A 
 &rarr\;<br>[0\, 1]) &rarr\; [0\, 1]. This allows to use Moggi&rsquo\;s mon
 adic&nbsp\;meta- language<br>to give an interpretation of a language\, Rml
 \, into type theory.<br>Rml is a functional language with a primitive for&
 nbsp\;probabilistic<br>choice. This formalization was the basis for the<br
 ><br>&nbsp\;&nbsp\;&nbsp\;&nbsp\; Certicrypt<br>system for verifying secur
 ity protocols. Easycrypt is still based on<br>the same idea. We improve on
  the formalization by&nbsp\;using homotopy<br>type theory which provides e
 .g. quotients and&nbsp\;functional<br>extensionality. Moreover\, homotopy 
 type theory allows us to use<br>synthetic topology to present a theory whi
 ch also&nbsp\; includes<br>continuous data types\, like [0\, 1]. Such data
  types are&nbsp\;relevant\, for<br>instance\, in machine learning and diff
 erential privacy.&nbsp\; We indicate how our axioms are justified by&nbsp\
 ; Kleene-Vesley<br>realizability\, a standard model for computation&nbsp\;
 with<br>continuous data types. (Joint work with Florian Faissole.)
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR