The Coq mailing list

[Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>]

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

regards,

Jean-Yves

http://www.cs.kun.nl/~freek/comparison/ 
<http://www.cs.kun.nl/%7Efreek/comparison/>
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