Further Scaling of Isabelle Technology

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

  1. Editing: Prover IDE,
  2. Building: batch-mode tools and background services,
  3. Browsing: HTML views and client-server applications.