
Coq
 Referenced in 1856 articles
[sw00161]
 formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms ... semiinteractive development of machinechecked 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 computerchecked proofs developed using the proof assistant Isabelle. We perform...

LCF
 Referenced in 157 articles
[sw08360]
 original LCF system was a proofchecking 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 computerchecked proof of the Four Colour Theorem and which...

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

CompCert
 Referenced in 48 articles
[sw09737]
 compilers come with a mathematical, machinechecked 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 FirstOrder Logic. This case study shows how nonACL2 ... results of the nonACL2 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 machinechecked proof of soundness of our Separation Logic. This ... first largescale machinechecked proof of a Separation Logic w.r.t. a smallstep semantics...

Toolchain
 Referenced in 25 articles
[sw09517]
 Software Toolchain project assures with machinechecked 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...

DRATtrim
 Referenced in 34 articles
[sw13313]
 DRATtrim: efficient checking and trimming using expressive clausal proofs. The DRATtrim tool ... proof checker based on the new DRAT proof format. Unlike its predecessor, DRUPtrim ... validated using DRATtrim. 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 semiformal 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 offtheshelf ... 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...

Psicalculi
 Referenced in 11 articles
[sw28573]
 formalisation is to keep the machine checked proofs as close to their penandpaper...