
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 computerchecked 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 wellfounded 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 wellfounded (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 correctbyconstruction ... 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 theoremproving tool...

Coquelicot
 Referenced in 12 articles
[sw11552]
 Coquelicot: A userfriendly 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 userfriendly 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 firstorder automated theorem ... deanonymization of abstract terms. Full Mizar proofs are now exported and also encoded ... prooflocal constants and prooflocal lemmas and translating of a number of Mizar proof ... constructs into the TPTP formalism. The proofs using secondorder 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...