coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq & Java applet

From: Thery Laurent <thery AT ns.di.univaq.it>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Coq & Java applet
Date: Tue, 25 Nov 2008 10:34:37 +0100 (CET)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

For those who may be interested on building java applets on top
of extracted Coq code, I've just discovered the ocamljava project:

http://ocamljava.x9c.fr/

This works pretty well (performance is not outstanding though).
Here is an example with my Sudoku solver

http://www-sop.inria.fr/marelle/Laurent.Thery/Sudoku/Sudoku.html

--
Laurent

[Coq-Club] Definitions inside type class definitions (Coq 8.2beta), Brian Aydemir
- Re: [Coq-Club] Definitions inside type class definitions (Coq 8.2beta), Matthieu Sozeau
- [Coq-Club] Coq & Java applet, Thery Laurent