• Coq/SSReflect

  • Referenced in 66 articles [sw09360]
  • Ssreflect extension library for the Coq proof assistant. The name Ssreflect stands for ”small scale ... proof that evolved from the computer-checked proof of the Four Colour Theorem and which ... provide effective automation for many small, clerical proof steps. This is often accomplished by restating ... name. For example, in the Ssreflect library arithmetic comparison is not an abstract predicate...
  • CoLoR

  • Referenced in 38 articles [sw09806]
  • CoLoR: a Coq library on well-founded rewrite relations and its application to the automated ... notably required for programs formulated in proof assistants. It is a very active subject ... library formalising important results of the theory of well-founded (rewrite) relations in the proof ... assistant Coq. We also present its application to the automated verification of termination certificates...
  • Agda

  • Referenced in 190 articles [sw09689]
  • many similarities with other proof assistants based on dependent types, such as Coq, Epigram ... README). Note that the Agda library does not follow the package versioning policy, because...
  • Fiat

  • Referenced in 14 articles [sw21357]
  • Fiat is a library for the Coq proof assistant for synthesizing efficient correct-by-construction ... program, which can be written using libraries of specification languages for describing common programming tasks ... Each derivation in Fiat produces a formal proof trail certifying that the synthesized program meets...
  • Whelp

  • Referenced in 14 articles [sw32446]
  • instantiated to the standard library of the Coq proof assistant extended with many user contributions...
  • Coquet

  • Referenced in 6 articles [sw09919]
  • hardware circuits in the Coq proof assistant. This library allows one to easily build circuits...
  • RedHom

  • Referenced in 12 articles [sw08776]
  • particular cubical complexes and simplicial complexes. The library is oriented on users who just need ... constitutes a part of CAPD (Computer Assisted Proofs in Dynamics) project. We decided to make ... RedHom available also as a seperate library, because the area of its applicability turned...
  • GeoCoq

  • Referenced in 8 articles [sw32242]
  • system. This library contains a formalization of geometry using the Coq proof assistant. It contains...
  • evt

  • Referenced in 7 articles [sw09805]
  • theorem prover which assists in obtaining proofs that ERLANG applications satisfy their correctness requirements formulated ... discuss reasoning principles essential for successful proofs such as inductive and compositional reasoning ... program libraries is outlined. EVT is essentially a classical proof assistant, or theorem-proving tool...
  • Coquelicot

  • Referenced in 12 articles [sw11552]
  • Coquelicot: A user-friendly library of real analysis for Coq. Real analysis is pervasive ... such, its support is warranted in proof assistants, so that the users have ... library of theorems on real analysis. Unfortunately, this standard library is lacking some widely used ... inadequacies, we have designed a user-friendly library: Coquelicot. An easier way of writing formulas...
  • A3PAT

  • Referenced in 8 articles [sw21587]
  • Coccinelle library formalises numerous rewriting techniques and termination criteria for the Coq proof assistant...
  • Proviola

  • Referenced in 10 articles [sw00737]
  • proof assistant (PA), in particular for storage and replay of proofs, we introduce three related ... concepts, those of: a proof movie, consisting of frames which record both user input ... uncouple the reviewing of a formal proof from the PA used to develop ... load a whole library into it.\parOther advantages include the possibility to develop a separate...
  • IsarMathLib

  • Referenced in 2 articles [sw22729]
  • IsarMathLib: A library of formalized mathematics for Isabelle/Isar proof assistant. In formalized mathematics definitions...
  • DAMPAS

  • Referenced in 1 article [sw31000]
  • relation to the Loco library, written in Coq proof assistant, dedicated to formal proofs...
  • Kami

  • Referenced in 4 articles [sw28644]
  • world to verify functional programs in proof assistants using induction, algebraic simplification, and rewriting ... this paper, we introduce Kami, a Coq library that enables similar expressive and modular reasoning...
  • MPTP 0.2

  • Referenced in 45 articles [sw02589]
  • make the large formal Mizar Mathematical Library (MML) available to current first-order automated theorem ... deanonymization of abstract terms. Full Mizar proofs are now exported and also encoded ... proof-local constants and proof-local lemmas and translating of a number of Mizar proof ... constructs into the TPTP formalism. The proofs using second-order Mizar schemes are now handled...
  • Mathematical Components

  • Referenced in 4 articles [sw30935]
  • Mathematical components library: The Mathematical Components Library is an extensive and coherent repository of formalized ... based on the Coq proof assistant, powered with the Coq/SSReflect language. These formal theories cover ... formal theories used in a formal proof of the Four Colour Theorem (Appel - Haken ... finite group theory, which utilizes the library extensively...
  • Coqtail

  • Referenced in 1 article [sw32382]
  • library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly...
  • NLCertify

  • Referenced in 4 articles [sw08786]
  • function f as input, NLCertify provides OCaml libraries that produce nonnegativity certificates for f over ... ultimately proved correct inside the Coq proof assistant. One specific challenge of the field...
  • FoCaLiZe

  • Referenced in 10 articles [sw12384]
  • file for the Coq proof assistant to check the proofs, a source file ... executable program. The FoCaLiZe distribution includes a library of mathematical algebraic structures up to multivariate...