• Isar

  • Referenced in 145 articles [sw04599]
  • Together with the Isabelle/Isar instantiation of Proof General, a generic (X)Emacs interface for interactive...
  • Proof General

  • Referenced in 53 articles [sw04901]
  • Proof General: A generic tool for proof development. This note describes Proof General, a tool ... target of a proof development. Proof General provides a powerful user-interface with relatively little ... appearance for diverse proof assistants. par Proof General has a growing user base ... give a brief overview of what Proof General does and the philosophy behind it; technical...
  • INTOPT_90

  • Referenced in 306 articles [sw04705]
  • computationally executed proofs of the existence of feasible points generalizing Hansen and Walster’s pioneering...
  • ALF

  • Referenced in 67 articles [sw08603]
  • implementation of ALF, which is an interactive proof editor based on Martin-Löf’s type ... with explicit substitutions. ALF is a general purpose proof assistant, in which different logics...
  • IsaPlanner

  • Referenced in 30 articles [sw02047]
  • IsaPlanner being used with Isabelle and Proof General) It is based on the Isabelle theorem ... prover and the Isar language. The main proof technique written in IsaPlanner is an inductive...
  • Find

  • Referenced in 86 articles [sw21614]
  • proof of termination is treated as a separate exercise. Finally, some conclusions relating to general...
  • ML

  • Referenced in 524 articles [sw01218]
  • Meta Language’) is a general-purpose functional programming language. It has roots in Lisp ... ensures type safety – there is a formal proof that a well-typed ML program does...
  • Pinocchio

  • Referenced in 42 articles [sw10193]
  • Pinocchio, a built system for efficiently verifying general computations while relying only on cryptographic assumptions ... uses the evaluation key to produce a proof of correctness. The proof is only ... public verification key to check the proof. Crucially, our evaluation on seven applications demonstrates that ... additional feature, Pinocchio generalizes to zero-knowledge proofs at a negligible cost over the base...
  • ETPS

  • Referenced in 161 articles [sw06302]
  • facilities of TPS for constructing natural deduction proofs have been used under the name ETPS ... Mellon for a number of years. Students generally learn to use ETPS fairly quickly just ... writing the appropriate lines of the proof and checking that the rules can be used...
  • seL4

  • Referenced in 91 articles [sw15222]
  • first formal proof of functional correctness of a complete, general-purpose operating-system kernel. Functional...
  • Plastic

  • Referenced in 18 articles [sw07403]
  • courtesy of David Aspinall’s generic Proof General. Speed-wise, it compares favourably with similar...
  • Proof General Kit

  • Referenced in 11 articles [sw09684]
  • interactive proof. This paper introduces Proof General Kit, a framework for software components tailored...
  • LEGO

  • Referenced in 108 articles [sw09685]
  • LEGO is an interactive proof development system (proof assistant) designed and implemented by Randy Pollack ... Calculus of Constructions (CC), the Generalized Calculus of Constructions (GCC) and the Unified Theory ... LEGO is a powerful tool for interactive proof development in the natural deduction style...
  • IMPS

  • Referenced in 52 articles [sw09143]
  • interactive mathematical proof system intended as a general-purpose tool for formulating and applying mathematics ... process and human comprehension of the resulting proofs. An initial theory library contained over...
  • Isabelle/PIDE

  • Referenced in 13 articles [sw07185]
  • minor variations like the well-known Proof General / Emacs interface). Thus the fundamental question ... negatively due to accidental weaknesses of existing proof engines. The idea of “PIDE” (which means...
  • leanTAP

  • Referenced in 41 articles [sw09985]
  • constitutes a proof of the correctness of leanTAP. Next, the author generalizes the sequent calculus...
  • KeYmaera

  • Referenced in 48 articles [sw03709]
  • KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose...
  • HERMES

  • Referenced in 9 articles [sw00403]
  • induction and theorem proving provide a general proof strategy [9,4], but they are either...
  • zk-SNARK

  • Referenced in 13 articles [sw22495]
  • curves. Non-interactive zero-knowledge proofs of knowledge for general NP statements are a powerful ... additional property, {it succinctness}, requiring the proof to be very short and easy to verify...
  • GND.lib

  • Referenced in 7 articles [sw27230]
  • dimensional local domains. An algorithmic proof of General Neron Desingularization is given here...