
Coq
 Referenced in 1690 articles
[sw00161]
 Coq is a formal proof management system. It provides a formal language to write mathematical...

Automath
 Referenced in 388 articles
[sw07127]
 better known current ones are Nuprl and Coq...

Agda
 Referenced in 166 articles
[sw09689]
 assistants based on dependent types, such as Coq, Epigram and NuPRL. This package includes both...

Isar
 Referenced in 134 articles
[sw04599]
 kind of semiautomated reasoning systems include Coq, PVS, HOL, and Isabelle. Despite this success...

Flyspeck
 Referenced in 102 articles
[sw10277]
 mainly been used with the Coq theorem prover: we show that the system itself...

KRAKATOA
 Referenced in 84 articles
[sw03159]
 JAVA files and produces specifications for COQ and a representation of the JAVA semantics...

Coq/SSReflect
 Referenced in 60 articles
[sw09360]
 Ssreflect extension library for the Coq proof assistant. The name Ssreflect stands for ”small scale ... which leverages the higherorder nature of Coq’s underlying logic to provide effective automation...

CCoRN
 Referenced in 34 articles
[sw06752]
 Constructive Coq Repository at Nijmegen, CCoRN, aims at building a computer based library ... constructive mathematics, formalized in the theorem prover Coq. Background: There is a lot of mathematical ... partly practical (because we wanted to use Coq, which is a constructive theorem prover...

Ynot
 Referenced in 34 articles
[sw12334]
 describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about ... order, dependentlytyped programs with sideeffects. Coq already includes a powerful functional language that ... powerful type and abstraction mechanisms of Coq to build higherlevel reasoning mechanisms which...

CoLoR
 Referenced in 37 articles
[sw09806]
 CoLoR: a Coq library on wellfounded rewrite relations and its application to the automated ... founded (rewrite) relations in the proof assistant Coq. We also present its application...

Proof General
 Referenced in 50 articles
[sw04901]
 used for several interactive proof systems, including Coq, LEGO, and Isabelle. Support for others...

CiME
 Referenced in 38 articles
[sw09970]
 CiME3 is the production of traces for Coq. CiME3 is also developed by the participants...

Zenon
 Referenced in 19 articles
[sw06753]
 produce OCaml code for execution and Coq code for certification. Zenon can directly generate ... Coq proofs (proof scripts or proof terms), which can be reinserted in the Coq specifications...

Ott
 Referenced in 28 articles
[sw00663]
 compiles them into proof assistant code for Coq, HOL, and Isabelle/HOL, together with LaTeX code...

Flocq
 Referenced in 16 articles
[sw06800]
 Flocq (Floats for Coq) is a floatingpoint formalization for the Coq system. It provides ... also supports efficient numerical computations inside Coq...

Paco
 Referenced in 15 articles
[sw10885]
 Paco: A Coq Library for Parameterized Coinduction. Paco is a Coq library implementing parameterized coinduction ... library provides a tactic called ”pcofix”, replacing Coq’s primitive cofix and avoiding its syntactic...

Mtac
 Referenced in 13 articles
[sw13075]
 monad for typed tactic programming in Coq. Effective support for custom proof automation is essential ... Mtac, a lightweight but powerful extension to Coq that supports dependentlytyped tactic programming. Mtac ... access to all the features of ordinary Coq programming, as well ... touch the trusted kernel typechecker of Coq by encapsulating uses of these new tactical primitives...

cminor
 Referenced in 19 articles
[sw09739]
 paper has been carried out in the Coq proof assistant. It is a first step...

Coquelicot
 Referenced in 11 articles
[sw11552]
 userfriendly library of real analysis for Coq. Real analysis is pervasive to many applications ... theorems and correctness of critical systems. The Coq system comes with an axiomatization of standard ... Moreover, Coquelicot is a conservative extension of Coq’s standard library and we provide correspondence...