Sciweavers

Share
ESOP
2016
Springer

Probabilistic Functions and Cryptographic Oracles in Higher Order Logic

3 years 6 months ago
Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
This paper presents a shallow embedding of a probabilistic functional programming language in higher order logic. 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. Several examples demonstrate that our language is suitable for conducting cryptographic proofs.
Andreas Lochbihler
Added 03 Apr 2016
Updated 03 Apr 2016
Type Journal
Year 2016
Where ESOP
Authors Andreas Lochbihler
Comments (0)
books