Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Industrial applications of Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Industrial applications of Coq


chronological Thread 
  • 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




Archive powered by MhonArc 2.6.16.

Top of Page