The Coq mailing list

[bertot <Yves.Bertot AT inria.fr>]

On 16/4/14 5:09 PM, Nuno Gaspar wrote:
> Great stuff :-)
>
> Is there a report about this decision? I don't seem to find it on the 
> website...
>
> I would be curious to see what were the arguments of Coq over Isabelle..
If you go on the page

http://awards.acm.org/software_system/

and look at the "Nomination process", you will understand that the 
question of comparing Coq and Isabelle was probably not raised: they 
chose among software systems that had been nominated and had enough 
sponsors.  Of course, I don't know, but I doubt several systems in the 
same area of computer science get nominated the same year.

More positively, I think this is also a success for the whole area of 
interactive theorem proving, including Isabelle.  All these systems, 
Agda, Epigram, HOL, Hol-light, Isabelle, Mizar, PVS, Twelf, and probably 
a few others progressed together and benefited from each other's hard work.

Yves