• Flyspeck

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

  • Referenced in 37 articles [sw06752]
  • Constructive Coq Repository at Nijmegen, C-CoRN, 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 machine-checked, 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 object-oriented ... 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]
  • paramodulation-based 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 type-theoretic 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 first-order 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...