On Monday 05-Feb-2018, I will give a presentation about Further Scaling of Isabelle Technology at VU Amsterdam, invited by Jasmin Christian Blanchette. See also the official seminar website.
Abstract:
Over 32 years, Isabelle has made a long way from a small experimental proof assistant to a versatile platform for proof document development and maintenance. 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?
I will revisit these questions from the perspectives of
- Editing: Prover IDE,
- Building: batch-mode tools and background services,
- Browsing: HTML views and client-server applications.