25 citations · 25 across the 2 of their papers we have counts for
2 papers
cs.LO2026
Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
Sage Binder, Hanna Lachnitt, Katherine Kosaian
In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "app…
cs.LO2020★ 25 cited
Certified Quantum Computation in Isabelle/HOL
Anthony Bordg, Hanna Lachnitt, Yijun He
In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being…