The Coq mailing list

[Pierre-Yves Strub <pierre-yves AT strub.nu>]

Hi,

You have this WIP for *discrete* distributions:

https://github.com/math-comp/analysis/blob/master/altreals/distr.v

Best. Pierre-Yves.

2018-08-16 9:49 GMT+02:00 Soegtrop, Michael 
<michael.soegtrop AT intel.com>:
> Dear Lily,
>
>
>
> thanks for the pointer!
>
>
>
> I was also looking into https://github.com/EasyCrypt/certicrypt which
> contains https://www.lri.fr/~paulin/ALEA/ and https://github.com/rnrand/VPHL
> but these are not quite what I was looking for. I will have a look at FCF!
>
>
>
> Best regards,
>
>
>
> Michael
>
>
>
> From: 
> coq-club-request AT inria.fr
>  
> [mailto:coq-club-request AT inria.fr]
>  On Behalf
> Of ikdc
> Sent: Wednesday, August 15, 2018 10:32 PM
> To: 
> coq-club AT inria.fr
> Subject: Re: [Coq-Club] Probability / randomness frameworks in Coq
>
>
>
> Hi,
>
>
>
> Try taking a look at Adam Petcher's project "Foundational Cryptography
> Framework": https://github.com/adampetcher/fcf
>
>
>
> Lily
>
>
>
> On Aug 15, 2018 16:11, "Soegtrop, Michael" 
> <michael.soegtrop AT intel.com>
> wrote:
>
> Dear Coq Users,
>
>
>
> does someone have pointers to frameworks for working with probabilities,
> distributions, random variables, … in Coq?
>
>
>
> Best regards,
>
>
>
> Michael
>
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928
>
>
>
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928