ACM SIGPLAN Programming Languages Software and Software System Awards

In 2013, when the Rocq prover was known as Coq, the ACM SIGPLAN Programming Languages Software and Software System Awards were given to the initial Coq development team (Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chet Murthy, Yves Bertot, Pierre Castéran) for their work on the Coq proof assistant.