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.