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

CCoRN
 Referenced in 37 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 ... wanted to use Coq, which is a constructive theorem prover), but mainly because constructive mathematics...

CtCoq
 Referenced in 13 articles
[sw09972]
 provides a working environment for the Coq theorem prover. It has been developed following...

GeoView
 Referenced in 9 articles
[sw12328]
 tool that combines the Coq theorem prover with the dynamic geometry drawing tool GeoplanJ developed ... proofs are constructed and verified with Coq theorem prover. A dynamic figure is automatically associated...

Gmeta
 Referenced in 4 articles
[sw10110]
 generic infrastructure is implemented in the Coq theorem prover. Furthermore, due to GMeta’s modular...

Vellvm
 Referenced in 6 articles
[sw13286]
 framework is built using the Coq interactive theorem prover. It includes multiple operational semantics ... design, we extract an interpreter from the Coq formal semantics that can execute programs from...

VeriStar
 Referenced in 3 articles
[sw09393]
 checked static analyses equipped with efficient theorem provers are now within the reach of formal ... functional programming language embedded in the Coq theorem prover. By machinechecked, we mean ... proof in Coq that when the prover says “valid”, the checked entailment holds ... mean that when the static analysis+theorem prover says a C minor program is safe...

Zenon
 Referenced in 23 articles
[sw06753]
 proofs. We present Zenon, an automated theorem prover for first order classical logic (with equality ... Zenon is intended to be the dedicated prover of the Focal environment, an objectoriented ... produce OCaml code for execution and Coq code for certification. Zenon can directly generate...

FreeSpec
 Referenced in 1 article
[sw37554]
 compositional reasoning framework for the Coq theorem prover. SpecCert is a framework for specifying...

VeriSmall
 Referenced in 6 articles
[sw09788]
 paramodulationbased heap theorem prover. Our implementation is done in Coq and is extractable...

Mtac
 Referenced in 14 articles
[sw13075]
 monad for typed tactic programming in Coq. Effective support for custom proof automation is essential ... base logic of the accompanying theorem prover, or (b) rely on advanced typetheoretic machinery ... established theorem provers.par We present Mtac, a lightweight but powerful extension to Coq that supports...

miz3
 Referenced in 11 articles
[sw18631]
 proofs are scripts of commands, like in Coq) and the declarative style (where proofs ... procedural interactive theorem prover, regardless of its architecture and logical foundations. To show the viability...

Prooftree
 Referenced in 1 article
[sw17593]
 development in a theorem prover. It is currently being developed for Coq and Proof General...

ArchSAT
 Referenced in 2 articles
[sw32252]
 ArchSAT: An firstorder theorem prover with formal proof output. Archsat is an experimental SMT/McSat ... that proof to various formal proof formats: coq proof script, coq proof term, dedukti proof...

ekstrakto
 Referenced in 1 article
[sw32250]
 often call automated theorem provers to prove subgoals. However, each prover has its own proof ... translated to various proof assistants: Coq, HOL, Lean, Matita, PVS. We implemented a tool that ... reconstructs complete proofs in Dedukti using automated provers able to generate Dedukti proofs like ZenonModulo ... prover producing the trace, and it can use different provers to produce the Dedukti proof...

ACL2
 Referenced in 291 articles
[sw00060]
 ACL2 is both a programming language in which...

AXIOM
 Referenced in 173 articles
[sw00063]
 Axiom is a general purpose Computer Algebra system...

Cinderella
 Referenced in 153 articles
[sw00127]
 An Interactive Geometry Software. Besides support for dynamic...

Coq
 Referenced in 1906 articles
[sw00161]
 Coq is a formal proof management system. It...