Skip to Content.
Sympa Menu

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

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?


Chronological Thread 
  • From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
  • To: "coq-club AT inria.fr" <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 12:51:55 +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-f174.google.com
  • Ironport-phdr: 9a23:lNspqRSy+cKto9gfbgj7vu5pAtpsv+yvbD5Q0YIujvd0So/mwa64ZBSN2/xhgRfzUJnB7Loc0qyN4vumAzZLu8ba+DBaKdoXCE9D0Z1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/hKiO/MiZaAJRwTG5fLlaLROsrAyXuNNcyd9pLb90wR/UqFNJff5XzCVmPwTAsQz745KR+JvI6T8YkPM76spBSu2ufqA9RKZDSj8nKX0x5dbDuhzKTA/J7XwZBDZF2iFUChTIuUmpFqz6tTH347Jw
Of course, anything can be done,
1) using standard functions and proving that necessary distribution and properties follow from distributions of parameters
2) and then calling such functions with appropriate random parameters

Still, such approach is a bit restricting.

On Mon, Nov 21, 2016 at 11:59 AM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:
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


Archive powered by MHonArc 2.6.18.

Top of Page