Français
3. Rooster and its place in computing
In 2013, Coq received two awards from the Association for Computing Machinery (ACM), the SIGPLAN "Programming Languages Software Award" and the prestigious "Software System Award". The text accompanying this second award places Coq in the context of correct software production. The full text can be found on the ACM website :
"Coq, used for both mathematical theorems and software specifications, is a key technology for the production of certified software.
Significant results achieved with Coq include the proof of the Four Color Theorem, the development of CompCert (a fully verified compiler for C), the development at Harvard of a verified version of Google's fault isolation...
The Ultimate Scientific and Technical Reference
This article is included in
Software technologies and System architectures
This offer includes:
Knowledge Base
Updated and enriched with articles validated by our scientific committees
Services
A set of exclusive tools to complement the resources
Practical Path
Operational and didactic, to guarantee the acquisition of transversal skills
Doc & Quiz
Interactive articles with quizzes, for constructive reading
Rooster and its place in computing
Evolution
Bibliography
- (1) - - The CompCert compiler. http://compcert.inria.fr .
- (2) - - OCaml page. http://www.ocaml.org/...
The Ultimate Scientific and Technical Reference
