• Coq

  • Referenced in 1856 articles [sw00161]
  • formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms ... semi-interactive development of machine-checked proofs. Typical applications include the formalization of programming languages...
  • Agda

  • Referenced in 199 articles [sw09689]
  • interactive system for writing and checking proofs. Agda is based on intuitionistic type theory...
  • Archive Formal Proofs

  • Referenced in 169 articles [sw28613]
  • vast collection of computer-checked proofs developed using the proof assistant Isabelle. We perform...
  • LCF

  • Referenced in 157 articles [sw08360]
  • original LCF system was a proof-checking program developed at Stanford University by Robin Milner ... descendents of LCF is HOL, a proof assistant for higher order logic originally developed...
  • LEGO

  • Referenced in 107 articles [sw09685]
  • argument synthesis and universe polymorphism make proof checking more practical by bringing the level...
  • ETPS

  • Referenced in 158 articles [sw06302]
  • writing the appropriate lines of the proof and checking that the rules can be used ... essential logical problems underlying the proofs, and it gives them immediate feedback for both correct...
  • Coq/SSReflect

  • Referenced in 69 articles [sw09360]
  • proof that evolved from the computer-checked proof of the Four Colour Theorem and which...
  • HOL

  • Referenced in 563 articles [sw05492]
  • which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem ... implementing combinations of deduction, execution, and property checking...
  • CompCert

  • Referenced in 48 articles [sw09737]
  • compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly...
  • ALF

  • Referenced in 67 articles [sw08603]
  • containing placeholders. A modular type/proof checking algorithm for complete proof objects is presented ... such a way that the type checking problem is reduced to a unication problem...
  • CeTA

  • Referenced in 46 articles [sw06584]
  • many complex termination criteria. Hence generated proofs may be of tremendous size, which makes ... impossible) for humans to check those proofs for correctness.par In this paper ... theorem prover Isabelle/HOL to automatically certify termination proofs. To this end, we first formalized ... these techniques we developed an executable check which guarantees the correct application of that technique...
  • Ivy

  • Referenced in 37 articles [sw10279]
  • Preprocessor and Proof Checker for First-Order Logic. This case study shows how non-ACL2 ... results of the non-ACL2 programs are checked at run time by ACL2 functions ... ACL2 program to search for a proof or countermodel ... ACL2 program succeeds, ACL2 functions check the proof or countermodel. The top ACL2 function...
  • cminor

  • Referenced in 19 articles [sw09739]
  • concurrent extensions. We detail a machine-checked proof of soundness of our Separation Logic. This ... first large-scale machine-checked proof of a Separation Logic w.r.t. a small-step semantics...
  • Toolchain

  • Referenced in 25 articles [sw09517]
  • Software Toolchain project assures with machine-checked proofs that the assertions claimed...
  • Pinocchio

  • Referenced in 36 articles [sw10193]
  • produce a proof of correctness. The proof is only 288 bytes, regardless of the computation ... public verification key to check the proof. Crucially, our evaluation on seven applications demonstrates that...
  • DRAT-trim

  • Referenced in 34 articles [sw13313]
  • DRAT-trim: efficient checking and trimming using expressive clausal proofs. The DRAT-trim tool ... proof checker based on the new DRAT proof format. Unlike its predecessor, DRUP-trim ... validated using DRAT-trim. Checking time of a proof is comparable to the running time ... trim tool can emit trimmed formulas, optimized proofs, and new TraceCheck$^{ + }$ dependency graphs. We describe...
  • Naproche

  • Referenced in 12 articles [sw28307]
  • Naproche project (Natural language Proof Checking) studies the semi-formal language of mathematics from ... mathematical texts and adapted proof checking software which checks texts written...
  • EasyCrypt

  • Referenced in 31 articles [sw09738]
  • sequence of games and hints. Proof sketches are checked automatically using off-the-shelf ... theorem provers, and then compiled into verifiable proofs in the CertiCrypt framework. The tool supports...
  • Paco

  • Referenced in 20 articles [sw10885]
  • Prop), using which one can perform coinductive proofs in a more compositional and incremental fashion ... cofix and avoiding its syntactic guardedness checking of proof terms. We have found that pcofix...
  • Psi-calculi

  • Referenced in 11 articles [sw28573]
  • formalisation is to keep the machine checked proofs as close to their pen-and-paper...