The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Sergey, Ilya
Sent: Thursday, August 16, 2018 10:38 AM
To: coq-club AT 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: +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