6 citations · 7 across the 2 of their papers we have counts for
2 papers
cs.LO2025★ 1 cited
Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
Lukas Bartl, Jasmin Blanchette, Tobias Nipkow
Metis is an ordered paramodulation prover built into the Isabelle/HOL proof assistant. It attempts to close the current goal using a given list of lemmas. Typically these lemmas ar…
cs.PL2015★ 6 cited
Foundational Extensible Corecursion
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is…