coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "Sergey, Ilya" <i.sergey AT ucl.ac.uk>
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 08:37:58 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=i.sergey AT ucl.ac.uk; spf=None smtp.mailfrom=i.sergey AT ucl.ac.uk; spf=Pass smtp.helo=postmaster AT EUR03-DB5-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:tkzi2RwlYui/k9HXCy+O+j09IxM/srCxBDY+r6Qd2+IfIJqq85mqBkHD//Il1AaPAd2Fraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HSbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKiI5/m/UhMx+jq1boQ6uqBNkzoHOfI2VMeBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YDAfcPMvhCr4nyuVQPrQOyDhSvCuPryj5HnHH61rA93uQgCw3GxxIvH8gBsHvKrNT4L7oSXvyxzKXS1zrMc+la2Sr+6IXRdB0qvP+CXbV1ccXLyEkvERvIjlqRqYz5PzOVy/8Cv3KH4OpnUOKjk28nqwdtojexwscgkJTGiZwTx1vZ9it52J44KNKkREJhfNKoDJlduzuVOodsX88uXmBltD45x7EYo5K3YSYHxI4jyhPecfCLbomF7xH7WOafPzh1h25pdbe6ihmu7Eev1uLxW8yq31ZErSdJjNzBu3AX2BPO5MWKT+Vy80W81TuO0Q3Y9/tKLloulaXBLp4s2r4wmYQXsUTEBiL4l0v5grOKekgq4+Sm5fnqb7X/qp+bLIB7lBvyMqMzmsyjGus4NRUOX26G9uimzL3j50r5QKlUgfIqjqnZsZfaJcIBqq6+Hg9VzoIj6xG4DzelytgXgX4HLFdddBKGiYjmJU3OLej3APujmVigjStnyvLcMrDuGJnBM2XPnbb5cbZ48UFcyQ4zzd5F55JTD7EMOPPzVlXqtNPGFB85PBK7wub8BdVgyoweXXiDDbWFP6/IrF+I5fojI/OQa48NpDb9N/8l6ubygn8+gF8RZLWm3Z8KaH+jBflmOEWYYX/0gtgbC2sKvww+TPbriFKYSzJTaWyyDOoA4WRxA4W/SIzHW4qFgbqb3S79EIccLjRNDUnJGnP1fa2FXe0NYWScOJkyvCYDUO3rcII72hy/8Efbz6tuZKKA+2sDuIjs2cld+ubX0xg5syF3WZfOm1qRRn15yztbDwQ927py9BQkmwWzlJNgivkdLuR9ovZAUwM0L5nZlrUoFtv2HAvKOMqKGg7/HoeWRAopR9d0+OcgJl5nEoz73A3I22yjCPkIlO7TXcFmwufnx3H0Yv1F5TPG2a0m0wZ0b/Z1bTbjqoQisg/ZCsjOjlmTkLuseeIExinR+WyfzG2I+kZFTAp3VqaDVncaNBLb
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

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 <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