Open Source Coq Wins ACM Software System Award
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/