The Coq mailing list

[Claude Marche <Claude.Marche AT lri.fr>]

And also have a look a the Why tool (http://why.lri.fr) which is
specialized in software verification, and supports 6 or 7 different
backend theorem provers, including Coq, PVS

>>>>> "Jean-Yves" == Jean-Yves Vion-Dury 
>>>>>Â <jean-yves.vion-dury AT inrialpes.fr>
>>>>>  writes:

    Jean-Yves> This link could be of help to you, although certainly a bit 
out-dated 
    Jean-Yves> (at least with respect to coq !)

    Jean-Yves> regards,

    Jean-Yves> Jean-Yves

    Jean-Yves> http://www.cs.kun.nl/~freek/comparison/ ;
    Jean-Yves> <http://www.cs.kun.nl/%7Efreek/comparison/>
    Jean-Yves> Daniel Nagle wrote:

    >> To Whom it may Concern:
    >> I am a student working on a project involving the construction and 
    >> proving of theorems for use in software verification. Part of my brief 
    >> is to learn what specific theorem provers are best at doing and why. 
    >> Coq has been heartily recommended to me and I am wondering if someone 
    >> could point out a good source of information to on the theorem prover 
    >> that would perhaps help me answer the folloing questions.
    >> 
    >> What are the main advantages of Coq in comparison to other Theorem 
    >> Provers?
    >> What area's in Coq are weak in comparison to other theorem provers?
    >> Is it possible to interface Coq directly with another program through 
    >> other methods apart from pipes and standard I/O?
    >> 
    >> If you can help me with the above questions I posed I would be very 
    >> grateful.
    >> 
    >> All the best,
    >> Daniel Nagle.
    >> --------------------------------------------------------
    >> Bug reports: http://coq.inria.fr/bin/coq-bugs
    >> Archives: http://pauillac.inria.fr/pipermail/coq-club
    >> http://pauillac.inria.fr/bin/wilma/coq-club
    >> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
    >> 
    >> 


    Jean-Yves> --------------------------------------------------------
    Jean-Yves> Bug reports: http://coq.inria.fr/bin/coq-bugs
    Jean-Yves> Archives: http://pauillac.inria.fr/pipermail/coq-club
    Jean-Yves>           http://pauillac.inria.fr/bin/wilma/coq-club
    Jean-Yves> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
| Claude Marché           | 
mailto:Claude.Marche AT lri.fr
 |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  ;|
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |