Coq is a formal proof management system. 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. Typical applications include the formalization of programming languages semantics (e.g. the CompCert compiler certification project or Java Card EAL7 certification in industrial context), the formalization of mathematics (e.g. the full formalization of the 4 color theorem or constructive mathematics at Nijmegen) and teaching.
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Chrzaszcz, Jacek; Czarnik, Patryk; Schubert, Aleksy: A dozen instructions make Java bytecode (2011)
- Lochbihler, Andreas; Bulwahn, Lukas: Animating the formalised semantics of a Java-like language (2011)
- Fox, Anthony; Myreen, Magnus O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture (2010)
- Atkey, Robert: CoqJVM: An executable specification of the Java virtual machine using dependent types (2008)