The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Thu, Oct 19, 2006 at 03:44:37PM +0200, Xavier Leroy wrote:
> > Coq currently extracts certified programs to Haskell, ML, and Scheme
> > (and TopLevel).
> > Has there been any work on extracting Java programs from Coq proofs?
> 
> As Benjamin Grégoire mentioned, translating a functional language into
> Java is not straightforward, especially if you want the generated Java
> code to be somewhat efficient and idiomatic.
> 
> It has been attempted, though (search the Web for "sml2java"), and
> functional languages have also been compiled relatively successfully
> to JVM bytecode (Nick Benton's MLj, Bigloo's JVM back-end) or .NET
> bytecode (SML.Net, F#).
> 
> Polymorphism is a problem, but less so in Java 5.0.  The real killer
> is the Coq module system, esp. functors.
> 
> In summary, a Java back-end for Coq's extraction facility could make a
> good master's internship project, but would still be quite a hack.
> 

Hi

In fact, it's not the first time someone asks about Java extraction
for Coq. I can't find the exact reference for the moment, but such an
internship project was tried once. It was people from
Sophia-Antipolis, maybe Guillaume Dufay, but I find no trace on his
web page. You'd better ask Gilles Barthes if he recall such an
experiment. Anyway, at that time I was quite doubtful about a direct
translation from Coq to Java, and I never heard again of this work
afterwards. As Benjamin and Xavier have already mentionned, extracting
to Java might be doable (at least for some subset of Coq language),
but this would be quite unnatural. Using the natural correspondance
(known as Curry-Howard) between (intuitionistic) proofs and functional
programming is by far the easiest way to proceed, and if you really
want to end with imperative code, look indeed at things like Bigloo's
compiler or the other tools mentionned by Xavier.

Best regards, 

Pierre Letouzey