coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] What's the best way to extract programs that use random numbers?
Date: Mon, 21 Nov 2016 11:59:40 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ilmars.cirulis AT gmail.com; spf=Pass smtp.mailfrom=ilmars.cirulis AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f179.google.com
Ironport-phdr: 9a23:mMepzh3adiGArQ73smDT+DRfVm0co7zxezQtwd8ZsegWKvad9pjvdHbS+e9qxAeQG96KsLQe0aGM4/uoGTRZp83e4DZaKN0EfiRGoPtVtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaymUrLV2o680Pn38JnOaS1JgiC8aPV8Nl/++Q7Wr4wdhZZoAqc30BrA5HVSLbd432RtcHOXmr3m/Y+b/YR+9yVL86Yg88tJS768dKUiULhZFxwpNmk04IvgshyVHljH3WcVTmhDykkAOAPC9hyvBpo=

Hello,

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.

Thank you,

Ilmars

[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