coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Eduardo Gimenez" <Eduardo.Gimenez AT trusted-logic.fr>
- To: <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] Industrial applications of Coq
- Date: Mon, 5 Jan 2004 12:36:43 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Dear Coq Users,
In the last few years, I have been asked several
times by researchers, professors and even marketing staff,
about what are the most important "industrial applications" and "success stories" of Coq. Usually, I answer mentioning the two industrial applications that I have participated in (the specification of a Lustre to C translator developed and the proof of correctness of the loading, linking and execution of Java Card applications for smart cards), but I know there have been other ones in Dassault, Philipps, France Telecom and other companies. I wonder if we could write down a complete list of public industrial applications, with entries of the form: Description : a short paragraph describing what was
specified and proved.
Industrial Partners : the name of the company that supported the development Authors: people that was involved in it, and who could be contacted for getting further details Date : the date when the development was finished If you have used Coq in your company and are
interested in collaborating with this idea,
please send me an entry like that. I will compile them all and send the result to this mailing list. Best wishes,
Eduardo Gimenez |
- [Coq-Club] Industrial applications of Coq, Eduardo Gimenez
Archive powered by MhonArc 2.6.16.