Burkhart Wolff

Plugins for the Isabelle Platform: A Perspective for Logically Safe,
Extensible, Powerful and Interactive Formal Method Tools

This talk will start with an overview over the historical development
of the LCF-style prover paradigm. The story so far reaches from
the development of first proof-support components such as data-type
packages and function definition packages, the development of
automated proof search procedures inside and the safe integration
of external provers, the development of add-on tools for programming
language  verification and specification analysis, and the
long way to develop adequate proof presentation and GUI
technologies. The talk will conclude with an overview of the
most recent challenges for the Isabelle system, which is turning
into a Formal Tool Implementation Platform with asynchronous
and parallel evaluation in the core and a collaborative theory
development interface on the surface.