
F*
 Referenced in 20 articles
[sw27563]
 with the expressive power of a proof assistant based on dependent types. After verification ... combination of SMT solving and interactive proofs...

cminor
 Referenced in 19 articles
[sw09739]
 been carried out in the Coq proof assistant. It is a first step towards...

JProver
 Referenced in 13 articles
[sw09978]
 connectionbased theorem proving into interactive proof assistants. JProver is a firstorder intuitionistic theorem ... proof engine in interactive proof assistants with expressive constructive logics. This paper gives a brief...

GeoProof
 Referenced in 17 articles
[sw05737]
 GeoProof can communicate with the Coq proof assistant to perform automatic and interactive proofs...

Plastic
 Referenced in 18 articles
[sw07403]
 extensions, in the form of a proof assistant. Typed LF is a framework type theory ... interface, courtesy of David Aspinall’s generic Proof General. Speedwise, it compares favourably with...

Gappa
 Referenced in 18 articles
[sw04885]
 automatic tactic for the Coq proof assistant...

mural
 Referenced in 9 articles
[sw23627]
 support tool and a proof assistant. The book is based on papers which were written ... containing the complete specification of the proof assistant. The first two chapters give a general ... system. Chapters 36 describe the proof assistant in more detail. The third chapter ... walk into the specification of the proof assistant and assumes the reader to be familiar...

Whelp
 Referenced in 15 articles
[sw32446]
 standard library of the Coq proof assistant extended with many user contributions...

Fiat
 Referenced in 14 articles
[sw21357]
 library for the Coq proof assistant for synthesizing efficient correctbyconstruction programs from declarative ... Each derivation in Fiat produces a formal proof trail certifying that the synthesized program meets...

SAD
 Referenced in 14 articles
[sw09796]
 proof verification. In this paper a proof assistant called SAD is presented. SAD deals with...

Isabelle/PIDE
 Referenced in 13 articles
[sw07185]
 Isabelle/PIDE platform addresses the question whether proof assistants of the LCF family are suitable ... minor variations like the wellknown Proof General / Emacs interface). Thus the fundamental question ... tools. We use Scala to expose the proof engine in ML to the JVM world ... This shall ultimately lead to combined mathematical assistants, where the logical engine...

VeriML
 Referenced in 8 articles
[sw13522]
 inside a language with effects. Modern proof assistants such as Coq and Isabelle provide high ... order logic and supply explicit machinecheckable proof objects. Unfortunately ... large scale proof development in these proof assistants is still an extremely difficult and time ... task. One major weakness of these proof assistants is the lack of a single language...

Verasco
 Referenced in 11 articles
[sw19985]
 proved sound using the Coq proof assistant. Verasco’s proof guarantees, with mathematical certainty, that...

Coquelicot
 Referenced in 12 articles
[sw11552]
 such, its support is warranted in proof assistants, so that the users have ... help with the proof process, the library comes with a comprehensive set of theorems that...

RedHom
 Referenced in 12 articles
[sw08776]
 constitutes a part of CAPD (Computer Assisted Proofs in Dynamics) project. We decided to make...

CFML
 Referenced in 8 articles
[sw13287]
 about the characteristic formula using a proof assistant such as Coq. Our characteristic formulae improve ... practice to verify programs using existing proof assistants. Our technique has been applied to formally...

PROSPER
 Referenced in 25 articles
[sw10386]
 PROSPER toolkit. The PROSPER (Proof and Specification Assisted Design Environments) project advocates...

CertiCoq
 Referenced in 11 articles
[sw22728]
 core language of the Coq proof assistant. A provedcorrect compiler consists of a high...

FoCaLiZe
 Referenced in 10 articles
[sw12384]
 source file for the Coq proof assistant to check the proofs, a source file...

evt
 Referenced in 8 articles
[sw09805]
 theorem prover which assists in obtaining proofs that ERLANG applications satisfy their correctness requirements formulated ... outlined. EVT is essentially a classical proof assistant, or theoremproving tool, requiring users ... meaningful feedback about the current proof state, to assist users in taking informed proof decisions...