Andrew Gacek

We consider the prover interaction approach underlying Interactive Theorem Proving (ITP) Systems, such as e.g. ProofGeneral (an open, XML-based, textual exchange protocol) for Isabelle, as inadequate: Both for technological as well as conceptual reasons.Technologically, in its last version called PGIP, the protocol approach ended up to be feature-overloaded. Conceptually, the linear, "script-oriented", paradigm of proof-presentation does not fit anymore in the modern, asynchronous, distributed world, both in the user-side (large teams develop in a distributed manner complex theories) as well on the technological side (multi-core processors, multi-threading ITP-system kernels, asynchronously coupled external provers).

In this talk, we outline the PIDE project, that aims to bring together recent GUI-technologies for ITP (i3p, JEdit/Scala) with an asynchronous, distributed document model to be used to interface ITP's, ATP's and user interfaces. Current work on the implementation in Isabelle/ISAR is also sketched.