coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: ikdc <ikdc AT mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Probability / randomness frameworks in Coq
Date: Wed, 15 Aug 2018 16:31:36 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ikdc AT mit.edu; spf=Pass smtp.mailfrom=ikdc AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-6.mit.edu
Importance: Normal
Ironport-phdr: 9a23:1I6TwB11oYL4aqMjsmDT+DRfVm0co7zxezQtwd8Zse0UK/ad9pjvdHbS+e9qxAeQG9mDtbQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYghEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmhjoJOT07/2/XlMJ/j7hVrxOuqBNjzIDZe4GVO+Fkc6/BYd8WWWhMU8BMXCJBGIO8aI4PAvIAPeZbsobyu0YFoBy/BQmvGezg1iRFhnr33a0myeguDxzJ3BE5Et8IrX/aotL1NKIIXuC0yqnF1TrDb/JK2Tf99YjHaQotru2LXbJ1acbRyE8vFx/bgVWUs4DqIi2a2+IQuGaY9+ptTf+jhm09pwxzuDSix8QhhpPHi48V0lzI6CZ0zJwoKdGlVUJ3e8OoHIdUui2AKYd7TcIvTmd1sygg0LIGo4S0fC0SxZQn2RHfb/uHfpCV7RLmVeedODJ4i2hkeLK7nBa971SvxvTnVsaoyllKqCxFncfWtnwU1hHf8M2HSvph/ku7xzmAyh3T5vlFIUAyi6XbN4YszqMzm5YJs0nPBC77lUbsgKKYdkgo4u2o5P7mYrXiqJ+cLYh0igTmP6QvmcywHPg3PxMLX2ia5eSwzqPs8lDkQLlSlP05jrHZsIzGJcQcvqO2HwhV0p865xmjCzemzc8XkGIcLFNFfRKHl5LmN0vPIPD+F/e/gk6jnC1lx/DcbfXdBcDGKWGGm7P8d5587VRdwUw914Nx/ZVRX7ACLPm7Dk7yuNfwCx4ldQG43rC0W51GyooCVDfXUeeiO6TIvArQv7N9E6y3fIYQ/Q3FBb0g7v/qg2U+nA5PeKi1m5YbdSLhR6g0EwCieXPpx+w5PyISpANvHunrlBuPXSMBPy/vDZJ53SkyDcedNamGRo2ph+fYjiu+DNhTb2FCEV2HVGzjfoOCVu1JNmSXI9MnnzAZB+Cs

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

[Coq-Club] Probability / randomness frameworks in Coq, Soegtrop, Michael, 08/15/2018
- Re: [Coq-Club] Probability / randomness frameworks in Coq, ikdc, 08/15/2018
  - RE: [Coq-Club] Probability / randomness frameworks in Coq, Soegtrop, Michael, 08/16/2018
    - Re: [Coq-Club] Probability / randomness frameworks in Coq, Pierre-Yves Strub, 08/16/2018
- Re: [Coq-Club] Probability / randomness frameworks in Coq, Sergey, Ilya, 08/16/2018
  - RE: [Coq-Club] Probability / randomness frameworks in Coq, Soegtrop, Michael, 08/16/2018