• # Coq

• Referenced in 1913 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...
• # LCF

• Referenced in 158 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...
• # ETPS

• Referenced in 161 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...
• # HOL

• Referenced in 594 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...
• # 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 47 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 39 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...
• # Pinocchio

• Referenced in 42 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...
• # 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...
• # DRAT-trim

• Referenced in 37 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 13 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 33 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 22 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...