The Coq mailing list

[Pierre Neron <pierre.neron AT polytechnique.org>]

Hi everyone

I did an internship few years ago at Gemalto. They use coq for formal 
verification, particularly around the JavaCard platform, and they even 
publish a few things.
You can have a look at the publications of:
Quang-Huy Nguyen : 
http://www.informatik.uni-trier.de/~ley/pers/hd/n/Nguyen_0002:Quang_Huy.html
Boutheina Chetali : 
http://www.informatik.uni-trier.de/~ley/pers/hd/c/Chetali:Boutheina.html

We also published a paper on a formal model of a smart card web server in Coq 
(http://www.lix.polytechnique.fr/~neron/Publi/SCWS/scws_cardis.pdf).

I think people at Prove&Run also use Coq. 

Another application is the use of Coq to verify the B tool used by Siemens, 
see Melanie Jacquel work 
(http://www.informatik.uni-trier.de/~ley/pers/hd/j/Jacquel:M=eacute=lanie.html).

Pierre.

On 23 mai 2014, at 17:16, Jonathan 
<jonikelee AT gmail.com>
 wrote:

> I'd be interested in finding out if there are any funded open-source 
> projects to use Coq that are looking for help.  The open-source ones 
> couldn't hide how seriously they employ Coq.
> 
> I might be headed in the direction of starting such a project myself - but 
> I'd certainly want to know about others first.
> 
> -- Jonathan
> 
> On 05/23/2014 11:06 AM, Adam Chlipala wrote:
>> I think the risk here is that some companies will hint at more serious Coq 
>> use than they actually employ in real product-oriented activity, as a 
>> trick to pull in the best developers. ;)
>> 
>> On 05/23/2014 11:01 AM, David MENTRE wrote:
>>> Le 23/05/2014 16:43, Adam Chlipala a écrit :
>>>> And how is a random person meant to learn more about the details?
>>> 
>>> It is difficult. It is not usual habit for companies to talk about their 
>>> practices (and nowadays everything is "confidential" in a company).
>>> 
>>>> If I
>>>> spent a little time poking around their web sites, would I get a good
>>>> sense?
>>> 
>>> Probably not, for above reasons.
>>> 
>>> Most of the time I found those kind of information through direct 
>>> discussion or through a few lines in a slide.
>>> 
>>> For Trusted Labs, you'll find some basic information by googling "trusted 
>>> labs coq" or "trusted logic coq". But probably not detailed enough for an 
>>> advanced user like you.
>>> 
>>> Sincerely yours,
>>> david
>>> 
>> 
>