The Coq mailing list

[Mathieu Boespflug <mboes AT tweag.net>]

Hi Bas,

On Wed, Mar 03, 2010 at 12:41:39PM +0100, Bas Spitters wrote:
> Very interesting.
> I guess you are referring to your paper:
> http://www.lix.polytechnique.fr/~mboes/papers/padl10.pdf
> 
> Could you explain more about the status of your implementation for Coq?

We (Maxime Dénès and I) currently have a prototype that requires quite
a bit of manual intervention. It implements the conversion test by
spitting out ML files that can manually be compiled to native code by
calling ocamlopt on the command line. It works for testing the
convertibility of closed terms (ie with no axioms or section variables
in the context at the point of the conversion test). The code dealing
with variables is still in flux. We'll make a git repo publically
available very soon if you are interested in experimenting. By the end
of the week we should have a significantly more user-friendly version
for you to try.

> I would be keen to try it on our real number computations:
> Certified Exact Transcendental Real Number Computation in Coq (Russell 
> O'Connor)
> http://arxiv.org/abs/0805.2438
> A computer verified, monadic, functional implementation of the
> integral (Russell O'Connor, Bas Spitters)
> http://arxiv.org/abs/0809.1552

Great! We are always looking for new benchmarks. 

> In the latter paper we experimented with threaded execution of the
> extracted program.
> 
> Would your approach allow something similar?

I'm not sure what kind of parralelism you are seeking. Do you mean
checking independent parts of a proof in parralel or would like for an
expensive conversion test to be run on multiple cores at once? We have
not thought about parralelism yet, but I don't think our approach
poses any particular problems in that regard. It's conceivable that
specific Coq-level axioms be mapped to OCaml primitives for multicore
computation, as is possible during extraction.

Regards,

Mathieu