
Isabelle/HOL
 Referenced in 820 articles
[sw01569]
 Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... main application is the formalization of mathematical proofs and in particular formal verification, which includes...

Isabelle
 Referenced in 524 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... main application is the formalization of mathematical proofs and in particular formal verification, which includes...

Automath
 Referenced in 378 articles
[sw07127]
 type theoretical” line of proof assistants from which the better known current ones are Nuprl...

HOL Light
 Referenced in 253 articles
[sw06580]
 overview. HOL Light is an interactive proof assistant for classical higherorder logic, intended ... logical kernel. Despite this, it provides powerful proof tools and has been applied to some...

Agda
 Referenced in 155 articles
[sw09689]
 your code). Agda is also a proof assistant: It is an interactive system for writing ... many similarities with other proof assistants based on dependent types, such as Coq, Epigram...

LCF
 Referenced in 148 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...

Isar
 Referenced in 125 articles
[sw04599]
 generic (X)Emacs interface for interactive proof assistants, we arrive at a reasonable environment...

Archive Formal Proofs
 Referenced in 114 articles
[sw28613]
 computerchecked proofs developed using the proof assistant Isabelle. We perform an indepth analysis ... archive, looking at various properties of the proof developments, including size, dependencies, and proof style...

LEGO
 Referenced in 104 articles
[sw09685]
 interactive proof development system (proof assistant) designed and implemented by Randy Pollack in Edinburgh using ... LEGO is a powerful tool for interactive proof development in the natural deduction style...

KRAKATOA
 Referenced in 83 articles
[sw03159]
 postconditions, the CQQ proof assistant for modeling the program semantics and conducting the development...

Proof General
 Referenced in 49 articles
[sw04901]
 developing machine proofs with an interactive proof assistant. Interaction is based around a proof script ... effort, alleviating the need for a proof assistant to provide its own GUI, and providing ... uniform appearance for diverse proof assistants. par Proof General has a growing user base...

ALF
 Referenced in 61 articles
[sw08603]
 substitutions. ALF is a general purpose proof assistant, in which different logics can be represented...

Coq/SSReflect
 Referenced in 56 articles
[sw09360]
 Ssreflect extension library for the Coq proof assistant. The name Ssreflect stands for ”small scale...

Isabelle/ZF
 Referenced in 55 articles
[sw04973]
 Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... main application is the formalization of mathematical proofs and in particular formal verification, which includes...

CoLoR
 Referenced in 36 articles
[sw09806]
 notably required for programs formulated in proof assistants. It is a very active subject ... wellfounded (rewrite) relations in the proof assistant Coq. We also present its application...

Ott
 Referenced in 25 articles
[sw00663]
 formal mathematics of a proof assistant  make it much harder than necessary to work with ... such definitions and compiles them into proof assistant code for Coq, HOL, and Isabelle/HOL, together ... binding structures; and (3) compilation to proof assistant code. This has been tested in substantial ... large fragment of OCaml, with mechanised proofs of various soundness results. Our aim with this...

Ynot
 Referenced in 32 articles
[sw12334]
 axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher...

MizarMode
 Referenced in 15 articles
[sw01973]
 MizarMode  an integrated proof assistance tool for the Mizar way of formalizing mathematics The Emacs ... MizarMode and focuses on the proof assistance functions and tools available ... methods employed in tactical and programmable proof assistants, it makes the “proof code ... give an overview of these proofassistance tools and their integration in the MizarMode...

Jakarta
 Referenced in 18 articles
[sw01269]
 compiler that translates JSL specifications into proof assistants; the JaKarTa Automation Kit (JAK), a toolset ... support reasoning about executable specifications within proof assistants. Goal of the work is to derive...

Plastic
 Referenced in 18 articles
[sw07403]
 extensions, in the form of a proof assistant. Typed LF is a framework type theory ... interface, courtesy of David Aspinall’s generic Proof General. Speedwise, it compares favourably with...