The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

> 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.

Alternatively, there are ways to interoperate between Java and the
Caml code generated by extraction: look up O'Jacare and CamlJava.

- Xavier Leroy