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

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...

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

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

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...

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

JProver
 Referenced in 11 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...

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...

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

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

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

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...

Isabelle/PIDE
 Referenced in 12 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...

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...

Coquelicot
 Referenced in 11 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...

Proviola
 Referenced in 10 articles
[sw00737]
 existing models of interaction with a proof assistant (PA), in particular for storage and replay...

Hipster
 Referenced in 7 articles
[sw11223]
 Hipster: integrating theory exploration in a proof assistant. This paper describes Hipster, a system integrating ... theory exploration with the proof assistant Isabelle/HOL. Theory exploration is a technique for automatically discovering ... theory development. The second is proof mode, used in a particular proof attempt, trying...

evt
 Referenced in 7 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...