Coq received ACM SIGPLAN Programming Languages Software 2013 award
Submitted by herbelin on 30 Jun 2013 16:26 GMT
The development of Coq has been initiated in 1984 at INRIA by Thierry Coquand and Gérard Huet, then joined by Christine Paulin-Mohring and more than 40 direct contributors.
The first public release was CoC 4.10 in 1989. Extended with native inductive types, it was renamed Coq in 1991.
Since then, a growing community of users has shared its enthousiasm in the originality of the concepts of Coq and of its various features, as a richly-typed programming language and as an interactive theorem prover.
Look here for more on the award.