coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] What's the best way to extract programs that use random numbers?

From: Xavier Leroy <Xavier.Leroy AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] What's the best way to extract programs that use random numbers?
Date: Mon, 21 Nov 2016 13:01:52 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=xavier.leroy AT gmail.com; spf=Pass smtp.mailfrom=xavier.leroy AT gmail.com; spf=None smtp.helo=postmaster AT mail-wj0-f180.google.com
Ironport-phdr: 9a23:5S/5jh31In1m+EZ1smDT+DRfVm0co7zxezQtwd8Zse0fLfad9pjvdHbS+e9qxAeQG96KsLQe0KGN6ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMijexe61+IRu5oQjfq8UdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1iikIKiQ5/XnMisJtkqxbrhKvqR9xzYHab46aNuZxcKzGcNMGRmdMRNpdWzBPD46+aYYEEuoPPfxfr4n4v1YBrAGxBRetBOzx0D9Dm3n40rMg0+QmEQDNwQstENMUv3TKrdX6Kr0SXfqzwqbW1zXDaPNX1Cz86IjOaBAhoOuDUah+ccrL0EQiER7OgFuXqYzgJTyV1+INvnCa7+pmT+KvinQopxt/oji13sssjpPJhoMPxlDK7yV0xps+K96gSENjf9KoDJ9duzuZOoZ2WM8uXXxktDogxrEbupO3YDAGxZc5yxLFdfCKfYqF7gjhWeqMOzt0mXZodK+5ih2v60av0Pf8WdOx0FtSripKjN3MtncV2hzW8MeHS/998l6v2DaNywzf8+9ELV03mKbHMZIhzbkwlp0csUTHACD6gln5jKiTdkk8++io7froYqn+q5OCK4N5jhvyP6cul8ClH+g0LxQCU3KG9em/yLHv5Uj5T69Ljv0ynKnZqpfaJcEDq6+2GQBVzIcj5AilDzu81NQXg2MHLFVFeR+cgIjpPkvBIPH8Dfuln1uslzJry+jcPrL9GpXNMmTDkLD5cLlh7E5c0RM/wsxb55JJEb4MO+nzW0/0tNzAFBA1KQ20w+D9CNV8zIwSQ2yPArXKeJ/V5FSP/6ckJ/SGTI4Tojf0bfY/tND0inpsqVYDfKSzlb8acnepVqBWKluYbGCqptobFnYivwwkTeWshkfUAm0bXGq7Q69pvmJzM4mhF4qWHo0=

On 11/21/2016 10:59 AM, Ilmārs Cīrulis wrote:
> I am thinking about the best way to use Coq for extracting correct programs
> that uses random numbers? (Preferably, into Haskell.)
> Is there some good library for such purposes? Or, if there's not, what's the
> best literature / articles to get useful insights.

You could certainly program (in Coq) using a probability monad, which
should extract nicely to Haskell or to Caml.

To formally reason about your probabilistic programs, the following
Coq libraries and tools could help:
- Alea https://www.lri.fr/~paulin/ALEA/
- Certicrypt http://certicrypt.gforge.inria.fr/

Hope this helps,

- Xavier Leroy

[Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/21/2016
- Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/21/2016
- Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Xavier Leroy, 11/21/2016
  - Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/21/2016
    - Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/22/2016
      - Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/22/2016
        
        Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/22/2016