
Isar
 Referenced in 145 articles
[sw04599]
 current enduser setup is mainly for Isabelle/HOL. Together with the Isabelle/Isar instantiation of Proof...

Sledgehammer
 Referenced in 139 articles
[sw07047]
 discharge interactive proof obligations arising in Isabelle/HOL. We extended it with LEOII and Satallax...

Nominal Isabelle
 Referenced in 76 articles
[sw12055]
 Isabelle is a definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure...

Nitpick
 Referenced in 64 articles
[sw00622]
 Nitpick is a counterexample generator for Isabelle/HOL that builds on Kodkod, a SATbased first...

CeTA
 Referenced in 47 articles
[sw06584]
 this paper we use the theorem prover Isabelle/HOL to automatically certify termination proofs. To this...

Ott
 Referenced in 32 articles
[sw00663]
 proof assistant code for Coq, HOL, and Isabelle/HOL, together with LaTeX code for productionquality...

Transfer
 Referenced in 29 articles
[sw21009]
 Transfer: A Modular Design for Quotients in Isabelle/HOL. Quotients, subtypes, and other forms of type...

Lifting
 Referenced in 29 articles
[sw21010]
 Transfer: A Modular Design for Quotients in Isabelle/HOL. Quotients, subtypes, and other forms of type...

CCSL
 Referenced in 25 articles
[sw03357]
 logic either for PVS or for for Isabelle/HOL (in new style Isar syntax). After translation...

MaSh
 Referenced in 25 articles
[sw08206]
 automatic theorem provers in the proof assistant Isabelle/HOL. A key component, the relevance ﬁlter, heuristically...

Autoref
 Referenced in 15 articles
[sw12809]
 refinement. We present the Autoref tool for Isabelle/HOL, which automatically refines algorithms specified over abstract...

HOLBoogie
 Referenced in 14 articles
[sw00409]
 combines Boogie with the interactive theorem prover Isabelle/HOL. In particular, we present specific techniques combining...

Isabelle/UTP
 Referenced in 14 articles
[sw21184]
 unifying theories of programming (UTP) in Isabelle/HOL. UTP is a framework for the study, formalisation...

Isabelle/Circus
 Referenced in 13 articles
[sw15208]
 semantic theory of UTP based on Isabelle/HOL). We derive proof rules from this semantics...

Berlekamp Zassenhaus
 Referenced in 9 articles
[sw28596]
 factoring squarefree integer polynomials in Isabelle/HOL. We further adapt an existing formalization ... dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using Isabelle...

HOLZ
 Referenced in 11 articles
[sw02996]
 plugin of the generic theorem prover Isabelle/HOL (Version 2005). It allows for importing...

IsaFoR
 Referenced in 6 articles
[sw10106]
 functions in (a firstorder subset of) Isabelle/HOL by encoding them as term rewrite systems ... where all necessary properties are derived inside Isabelle/HOL without oracles. Apart from the certification ... reduction of the proof obligation produced by Isabelle/HOL to the termination of the corresponding term...

HOLTestGen
 Referenced in 10 articles
[sw17720]
 specfication and theorem proving environment Isabelle/HOL...

RALL
 Referenced in 9 articles
[sw08505]
 system is an advanced case study for Isabelle/HOL, and on the other hand, a quite...