[Coq-Club] Probability / randomness frameworks in Coq

[Soegtrop, Michael]

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: [phone], 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

[ikdc]

[Soegtrop, Michael]

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-***@inria.fr [mailto:coq-club-***@inria.fr] On Behalf Of ikdc
Sent: Wednesday, August 15, 2018 10:32 PM
To: coq-***@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" <***@intel.com<mailto:***@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: [phone], www.intel.de<http://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: [phone], 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

[Pierre-Yves Strub]

Hi,

You have this WIP for *discrete* distributions:

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

Best. Pierre-Yves.

Post by Soegtrop, Michael
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
Sent: Wednesday, August 15, 2018 10:32 PM
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
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: [phone], 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: [phone], 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

[Sergey, Ilya]

Dear Michael,

We are using Reynald Affeldt et al.’s infotheo framework:

https://github.com/affeldt-aist/infotheo

For some cool applications, check out “Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory” by Affeldt and Garrigue, ITP’15.

Kind regards,
Ilya

On 15 Aug 2018, at 21:11, Soegtrop, Michael <***@intel.com<mailto:***@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: [phone], www.intel.de<http://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

[Soegtrop, Michael]

Dear Sergey,

thanks for the pointer – I just had a first look and it also looks interesting!

What I am looking for is a formalization of probabilities, random variables, distributions, 
 which can be used in all fields which need them. As far as I can see currently independent formalizations exist for the use in information theory, cryptography and randomized algorithms. For most of these areas I can find even more than one formalization of probabilities and randomness. The area I wanted to look into is formalizing some statistical methods, e.g. hypothesis testing. There doesn’t seem to be much work in this area as yet.

Best regards,

Michael

From: coq-club-***@inria.fr [mailto:coq-club-***@inria.fr] On Behalf Of Sergey, Ilya
Sent: Thursday, August 16, 2018 10:38 AM
To: coq-***@inria.fr
Subject: Re: [Coq-Club] Probability / randomness frameworks in Coq

Dear Michael,


We are using Reynald Affeldt et al.’s infotheo framework:


https://github.com/affeldt-aist/infotheo


For some cool applications, check out “Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory” by Affeldt and Garrigue, ITP’15.


Kind regards,
Ilya
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], 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