> I think if your code
> [snip]
>
> This should be a proof that your code is pure ?

Sure, with some hackery this might be doable. And this would provide
an informal proof (weaker than something ensured by a (hopefully)
sound typechecker).

But the :

> - maybe one or two other conditions that I miss ?

will upset any Haskeller :-)

> Maybe someone could/has implement/ed a purity check for OCaml ? Or even
> better a patch to have
> the pure subset of OCaml with an optimized GC (no more list of greyval),
> that would be nice !

Indeed, that's would be very helpful. In fact, I was so desperate to
have to leave OCaml that I have considered a kind of "pure" (O)Caml.
But now that I'm sober, erf...

Nonetheless, that's an interesting food for thoughts.

> I think this would be a complete loss of time ! Moreover 2kloc is not so
> much so the referee could
> look at it ?

I have no experience as a referee as well as a "reviewed" (that's my
first submission in a FP conference) but I use to think that if things
are not clear, the referee will simply drop the paper.

And, as I mentioned, my functional structure is quite unusual so that
I have to be very convincing.

Thanks for your suggestions,
Best regards,

-- 
Pierre-Evariste DAGAND