coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]program extraction in Java?

From: Adam Megacz <megacz AT cs.berkeley.edu>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club]program extraction in Java?
Date: Wed, 11 Oct 2006 22:47:20 -0700
Cancel-lock: sha1:6HEyIDyqbUDZzdrbXJ50MGpBZXw=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: Myself

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

--
PGP/GPG: 5C9F F366 C9CF 2145 E770 B1B8 EFB1 462D A146 C380

[Coq-Club]program extraction in Java?, Adam Megacz
- Re: [Coq-Club]program extraction in Java?, Benjamin Gregoire
- Re: [Coq-Club]program extraction in Java?, Xavier Leroy
  - Re: [Coq-Club]program extraction in Java?, Pierre Letouzey
    - Re: [Coq-Club]program extraction in Java?, Thery Laurent
      - Re: [Coq-Club]program extraction in Java?, Virgile Prevosto