• Coq

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

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

  • Referenced in 144 articles [sw04599]
  • kind of semi-automated reasoning systems include Coq, PVS, HOL, and Isabelle. Despite this success...
  • Flyspeck

  • Referenced in 119 articles [sw10277]
  • mainly been used with the Coq theorem prover: we show that the system itself...
  • Coq/SSReflect

  • Referenced in 69 articles [sw09360]
  • Ssreflect extension library for the Coq proof assistant. The name Ssreflect stands for ”small scale ... which leverages the higher-order nature of Coq’s underlying logic to provide effective automation...
  • KRAKATOA

  • Referenced in 86 articles [sw03159]
  • JAVA files and produces specifications for COQ and a representation of the JAVA semantics...
  • C-CoRN

  • Referenced in 35 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 ... partly practical (because we wanted to use Coq, which is a constructive theorem prover...
  • Ynot

  • Referenced in 35 articles [sw12334]
  • describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about ... order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that ... powerful type and abstraction mechanisms of Coq to build higher-level reasoning mechanisms which...
  • CoLoR

  • Referenced in 38 articles [sw09806]
  • CoLoR: a Coq library on well-founded 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 53 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 23 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...
  • Paco

  • Referenced in 20 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...
  • Ott

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

  • Referenced in 19 articles [sw06800]
  • Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides ... also supports efficient numerical computations inside Coq...
  • Mtac

  • Referenced in 14 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 dependently-typed 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...
  • UniMath

  • Referenced in 18 articles [sw15140]
  • theories such as the ones used in Coq, Agda or Lean is based ... univalent style using a small subset of Coq language...
  • HoTT

  • Referenced in 15 articles [sw15147]
  • HoTT/HoTT Library in Coq: Designing for Speed. The HoTT/HoTT library is one of the major ... Coq libraries exploring univalent foundations and homotopy type theory, the other being UniMath. The library ... design choices and features, both of Coq and of univalent type theory, which allow...