Coq received ACM SIGPLAN Programming Languages Software 2013 award
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.