• 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. Speed-wise, 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 3--6 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]
  • connection-based theorem proving into interactive proof assistants. JProver is a first-order 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 correct-by-construction 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 machine-checkable 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 well-known 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 theorem-proving tool, requiring users ... meaningful feedback about the current proof state, to assist users in taking informed proof decisions...