The Coq mailing list

[Virgile Prevosto <virgile.prevosto AT m4x.org>]

Hello Laurent,
Le jeu 19 oct 2006 19:01:37 CEST,
Thery Laurent 
<thery AT ns.di.univaq.it>
 a écrit :

> 
> Virgile Prevosto had an extraction in Java back in 98.
> 

To be exact, it was in 99 (for Coq v6.3.1 if I'm not mistaken). I'm
afraid I don't have an electronic version of the report that I've
written at that time (maybe there's one lying around on some old hard
disk at INRIA Sophia-Antipolis), and it was in French anyway, but
basically what Benjamin and Xavier have said is true: partial
application, higher-order functions and polymorphism (especially for
the Java version of 1999) are not so easy to encode in Java, and the
generated code was neither really efficient nor elegant. But it's
certainly doable as an internship project.

-- 
E tutto per oggi, a la prossima volta.
Virgile