Showing cs.LOShow all
2 papers · 1 filter
cs.LO2020
Making Isabelle Content Accessible in Knowledge Representation Formats
Michael Kohlhase, Florian Rabe, Makarius Wenzel
The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adeq…
cs.LO2019
Isabelle technology for the Archive of Formal Proofs with application to MMT
Makarius Wenzel
This is an overview of the Isabelle technology behind the Archive of Formal Proofs (AFP). Interactive development and quasi-interactive build jobs impose significant demands of sca…