At the Dagstuhl-Seminar 23401 Automated mathematics: integrating proofs, algorithms and data (01..06-Oct-2023), I delivered a talk on Isabelle as System Platform for the Archive of Formal Proofs (AFP) .

Abstract:

Isabelle is usually seen as an interactive proof assistant, mostly for Higher-Order Logic (HOL), but that is somehow accidental. In reality, Isabelle is a system platform for functional programming and formal proofs, with sufficient infrastructure to carry its own weight and gravity. The Archive of Formal Proofs (AFP) is the official collection of Isabelle applications that is maintained together with the base system. That poses ever growing demands on the Isabelle platform. This talk gives an overviewof Isabelle software technology, with specific focus on Programming and Scaling, e.g. distributed build clusters for AFP.

See also the slides, which contain further links to relevant materials.