The Coq Proof Assistant

After the ACM SIGPLAN Programming Languages Sofware 2013 Award, Coq received the ACM Software System 2013 award.

The recipients of the award are thanking all developers who contributed to the success of Coq, the users who illustrated how to use Coq for so many impressive projects in formal certification, programming, logic, formalization of mathematics and teaching as well as the whole surrounding scientific community in proof theory, type theory, programming languages, interactive theorem proving.

All over 30 years, Coq also benefited from the trust and support from Inria and from its partners, CNRS, ENS Lyon, University Paris-Sud, École Polytechnique, University Paris-Diderot.