Thursday 20 June 2019, 14:00, LSV library: Isabelle technology for the Archive of Formal Proofs, 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 scalability on the logic (usually Isabelle/HOL), on Isabelle/ML for mathematical tool implementation, and on Isabelle/Scala for physical system integration --- all integrated in Isabelle/PIDE (the Prover IDE). Continuous growth of AFP (since 2004) has demanded continuous improvements of Isabelle performance. This is a report on the situation in Isabelle2019 (June 2019), with notable add-ons like prover session exports and headless PIDE for automated updates based on semantic information. An example application is Isabelle/MMT, which is able to turn all of Isabelle + AFP into OMDoc and RDF triples, but it is easy to reuse the Isabelle technology for other applications.

For more details, see here.