Scaling Isabelle Proof Document Processing

Isabelle applications (e.g. from AFP) are growing steadily in size and number. To outline requirements and possibilities of the technology, I have produced a document on Scaling Isabelle Proof Document Processing.

Abstract:

This is a study of performance requirements, technological side-conditions, and possibilities for scaling of formal proof document processing in Isabelle and The Archive of Formal Proofs (AFP). The approaches range from simple changes of system parameters and basic system programming with standard APIs to more ambitious reforms of Isabelle and the underlying Poly/ML system. The running examples for typical scalability issues are existing formalizations of classical analysis and differential equations. Such applications can be further extrapolated towards a development of Financial Mathematics (e.g. Itô calculus).