
Isabelle/HOL
 Referenced in 921 articles
[sw01569]
 Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...

Isabelle
 Referenced in 594 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...

Automath
 Referenced in 396 articles
[sw07127]
 computer. It’s the direct ancestor of the ”type theoretical” line of proof assistants from...

Archive Formal Proofs
 Referenced in 139 articles
[sw28613]
 vast collection of computerchecked proofs developed using the proof assistant Isabelle. We perform...

LCF
 Referenced in 157 articles
[sw08360]
 history. The original LCF system was a proofchecking program developed at Stanford University ... form a thriving paradigm in computer assisted reasoning. Many of the developments of the last ... descendents of LCF is HOL, a proof assistant for higher order logic originally developed...

RedHom
 Referenced in 12 articles
[sw08776]
 RedHom constitutes a part of CAPD (Computer Assisted Proofs in Dynamics) project. We decided...

Coq/SSReflect
 Referenced in 62 articles
[sw09360]
 proof assistant. The name Ssreflect stands for ”small scale reflection”, a style of proof that ... evolved from the computerchecked proof of the Four Colour Theorem and which leverages...

KRAKATOA
 Referenced in 85 articles
[sw03159]
 distinct components: the WHY tool, which computes proof obligations for a core imperative language annotated ... postconditions, the CQQ proof assistant for modeling the program semantics and conducting the development...

LorenzDatabase
 Referenced in 5 articles
[sw14477]
 guarantees their existence via computerassisted proofs methods. The orbits are computed using highprecision...

Isabelle/ZF
 Referenced in 61 articles
[sw04973]
 Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...

CoqMT
 Referenced in 5 articles
[sw19139]
 extension of the Coq proof assistant incorporating, in its computational mechanism, validity entailment for user ... provides more automation during the development of proofs. CoqMT improves over the Calculus of Congruent...

MahonianStat
 Referenced in 11 articles
[sw06180]
 proofs that the distribution is asymptotically normal. The first is computerassisted, based ... perform experiments and calculations. Our second proof uses characteristic functions. We then take...

Isar
 Referenced in 138 articles
[sw04599]
 proof documents sets out to bridge the semantic gap between internal notions of proof given ... broad range of automated proof methods. Interactive proof development is supported directly as well ... Theories, theorems, proof procedures etc. may be used interchangeably between Isabelleclassic proof scripts ... instantiation of Proof General, a generic (X)Emacs interface for interactive proof assistants, we arrive...

Octave Interval
 Referenced in 1 article
[sw13236]
 Also it can be applied to computerassisted proofs, constraint programming, and verified computing...

MMTTeX
 Referenced in 2 articles
[sw31595]
 contentoriented ones such as proof assistants and computer algebra systems on the other hand...

VeriML
 Referenced in 8 articles
[sw13522]
 typed computation of logical terms inside a language with effects. Modern proof assistants such ... task. One major weakness of these proof assistants is the lack of a single language ... manner. This limits the scalability of the proof development process, as users avoid developing domain ... design that couples a typesafe effectful computational language with firstclass support for manipulating...

Ynot
 Referenced in 35 articles
[sw12334]
 axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher ... call Ynot, is the added support for computations that may have effects such...

CFML
 Referenced in 8 articles
[sw13287]
 about the characteristic formula using a proof assistant such as Coq. Our characteristic formulae improve ... Honda} et al.’s [Lect. Notes Comput. Sci. 4052, 360371 (2006; Zbl 1133.03333)] total ... practice to verify programs using existing proof assistants. Our technique has been applied to formally...

GEX
 Referenced in 33 articles
[sw09961]
 used to build dynamic visual models to assist teaching and learning of various mathematical concepts ... Geometry Expert (GEX) is a powerful computer program for geometric reasoning. Within its domain ... prrperties of theorems, and to generate readable proofs for mant geometry throerms. 2) By dynamic...

TRX
 Referenced in 9 articles
[sw08800]
 interpreter. Parsing is an important problem in computer science and yet surprisingly little attention ... parser interpreter formally developed in the proof assistant Coq, capable of producing formally correct parsers...