• 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 higher-order 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 proof-checking 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]
  • computer-checked proofs developed using the proof assistant Isabelle. We perform an in-depth 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]
  • post-conditions, 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 ... well-founded (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 proof-assistance 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. Speed-wise, it compares favourably with...