14 Jul 2016 - Andreas Lochbihler

Abstract

In this talk, I am going to present a shallow embedding of a probabilistic functional programming language in higher order logic. The language yields a framework for conducting cryptographic proofs in the computation model and having them checked by a theorem prover. The language features monadic sequencing, recursion, random sampling, failures and failure handling, and black-box access to oracles. Oracles are probabilistic functions which maintain hidden state between different invocations. To that end, we propose generative probabilistic systems as the semantic domain in which the operators of the language are defined. We prove that these operators are parametric and derive a relational program logic for reasoning about programs from parametricity.