FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Further Scaling of Isabelle Technology

Author: Makarius Wenzel

Paper Information

Title:Further Scaling of Isabelle Technology
Authors:Makarius Wenzel
Proceedings:Isabelle Papers
Editor: Makarius Wenzel
Keywords:Scaling, Isabelle, Technology
Abstract:

ABSTRACT. Over 32 years, Isabelle has made a long way from a small experimental proof assistant to a versatile platform for proof document development. There has always been a challenge to keep up with the natural growth of applications, notably the Archive of Formal Proofs (AFP). Can we scale this technology further, towards really big libraries of formalized mathematics? Can the underlying Scala/JVM and Poly/ML platforms cope with the demands? Can we eventually do 10 times more and better? In this paper I will revisit these questions particularly from the perspective of: * Editing: Prover IDE infrastructure and front-ends, * Building: batch-mode tools and background services, * Browsing: HTML views and client-server applications.

Pages:17
Talk:Jul 13 12:00 (Session 86E: Isabelle 2)
Paper: