Open Source Coq Wins ACM Software System Award

By Renee Dopplick, ACM Director of Public Policy

April 16, 2014

ACM today selected open source Coq as the recipient of the ACM Software System Award for its influential and critical role as a primary programming and certification tool.

Coq is a software tool for the interactive development of formal theorem proofs and is written in open source OCaml. It provides a formal language to write mathematical definitions, executable algorithms, and theorems together with an environment for semi-interactive development of machine-checked proofs. It uses logic known as the calculus of inductive constructions.

Coq has played an influential role in formal methods, programming languages, program verification, and formal mathematics. It is a key enabling technology for certified software.

To learn more about the ACM Software System Award, visit http://awards.acm.org/software_system/