The Coq mailing list

[Benjamin Gregoire <Benjamin.Gregoire AT sophia.inria.fr>]

Adam Megacz 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?
>
>  - a
>
>  

Coq is a functional language so it allow partial application and local 
definition of functions.
It is not impossible to encode partial application using JAVA, but not 
simpl.
Furthermore, I think that polymorphism in JAVA is problematic.
But from C you can call OCaml function, and from JAVA you can call C 
function.
Since you can extract Coq to Caml you have a way to extract Coq to JAVA,
 Good luke :).

B.