The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Using Coq 8.5, I get error in the file Ccpo.v (of Alea, version 8), line 1729

> apply (fmonotonic2 F); auto.

> Unable to unify "monotonic2 (fun2 F)" with

>  "(F (mlub cte nat k)) (lub h) <= lub (F k @ h)".

I will try to fix it myself, of course, but I will be thankful for any hints. :)

On Mon, Nov 21, 2016 at 6:31 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Big thank you!

Yes, it helps.

It seems that Alea must be ported to Coq 8.5, but that seems easy to do. In progress.

--

Ilmars

On Mon, Nov 21, 2016 at 2:01 PM, Xavier Leroy <Xavier.Leroy AT inria.fr> wrote:

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