Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] Probability / randomness frameworks in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Probability / randomness frameworks in Coq


Chronological Thread 
  • From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: RE: [Coq-Club] Probability / randomness frameworks in Coq
  • Date: Thu, 16 Aug 2018 07:49:42 +0000
  • Accept-language: de-DE, en-US
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga03.intel.com
  • Ironport-phdr: 9a23:VGWzxBOBln2sUBmLpuUl6mtUPXoX/o7sNwtQ0KIMzox0IvT9rarrMEGX3/hxlliBBdydt6oazbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlJiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkHKTA37X3XhMJzgqJVoh2hpgBwzIHPbY6PKPZzernQcc8GSWdDWMtaSixPApm7b4sKF+cNM/tWr47jqFsBsRu+Hw6sBPv3xjRVgXH23LE10+Q7Hg7Y2AwsEc8FvXPRrNX0KKgSUfq6w7fMzTnZdPNW3iny6IfUchA7pvGMRal9ccvXyUkzCQzFik+cppDiPzOQz+kAtXWQ4eRnVeKqkWEnqgdxryCgxsctlonJhp8VxUve+Splx4Y1IMW0SE99Yd64DpRQszuWOJZoTc86R2Fooic6xqcIuZ6heiUB1ZcpxwbHZvCafYWF7QjvWPufLDp3nn5pZbyyiheo/UWhyuDwTtS43VdEoyZfnNTBuGoB2wLd58WDUPdx40Ss1SiX2wzO6+xJJVo4mbTbJpMu2LI8iIAfvVnAEyPqnkj9kbWYeV8++uey7uTqerXmqYGYN49zkgz+N6suldajDek2KAQOXm6b+fii273n50H2XLJKjvgunqnYtpDVO9gbq7akDwJb3Ysv8QuzAjmp3dgCgHUKIlNIdAiGgoXpI13OJer3Dfa7g1SiijdrwPXGM6XkApXMMnfDkK3ucqh560JG0wozys5Q551ICrEbJ/LzQlT8tN3eDh8lLQO0x/zrB8l61oMbQW6PGLOWMLvOsV+U4eIiO/WDZIgMuDrkN/cl4+PugmQilF8Gfaip2IMXZ2qiEvRnJUWZe3vsjc0bHWcEpAptBNDt3ReJVicWbHKvVYo94Cs6AcSoF82LEouqmfmK2DqxNpxQfGFPTF6WRyTGbYKBDr03by+dPtVminhMcLmqS4Ys0Vvm4Ar7wLpuI+6S4SoVuo7508Bd5uvPmBV0/jtxWZfOm1qRRn15yztbDwQ927py9BQkmwWzlJNgivkdLuR9ovZAUwM0L5nZlrUoCtbuVwaHddCMGg//HoeWRAopR9d0+OcgJl5nEoz73BHFwyeuRbQSku7TXcFmwufnx3H0Yv1F5TPG2a0m1gZ0R8RGbTbgh6hj+gyVDInMwR2U

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


Archive powered by MHonArc 2.6.18.

Top of Page