
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 userinterface 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 MartinLö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 generalpurpose functional programming language. It has roots in Lisp ... ensures type safety – there is a formal proof that a welltyped 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 zeroknowledge 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, generalpurpose operatingsystem kernel. Functional...

Plastic
 Referenced in 18 articles
[sw07403]
 courtesy of David Aspinall’s generic Proof General. Speedwise, 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 generalpurpose 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 wellknown 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 freevariable 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...

zkSNARK
 Referenced in 13 articles
[sw22495]
 curves. Noninteractive zeroknowledge 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...