[Club2] Talk by Makarius Wenzel on July 29

[Lukas Bulwahn]

Dear all,


Makarius will visit us on July 29 and July 30 and give a talk on

     Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit

(see abstract below). It will take place tomorrow, July 29, at 10:00 in room 01.11.018 (Zuse) in Garching.


Lukas



Abstract:

After several decades, most proof assistants are still centered around
TTY-based interaction in a tight read-eval-print loop.  Even well-known
Emacs modes for such provers follow this synchronous model based on single
commands with immediate response, meaning that the editor waits for the
prover after each command.  There have been some attempts to re-implement
prover interfaces in big IDE frameworks, while keeping the old interaction
model.  Can we do better than that?

Ten years ago, the Isabelle/Isar proof language already emphasized the
idea of proof document (structured text) instead of proof script (sequence
of commands), although the implementation was still emulating TTY
interaction in order to be able to work with the then emerging
Proof~General interface.  After some recent reworking of Isabelle
internals, to support parallel processing of theories and proofs, the
original idea of structured document processing has surfaced again.

Isabelle versions from 2009 or later already provide some support for
interactive proof documents with asynchronous checking, which awaits to be
connected to a suitable editor framework or full-scale IDE.  The remaining
problem is how to do that systematically, without having to specify and
implement complex protocols for prover interaction.

This is the point where we introduce the new Isabelle/Scala layer, which
is meant to expose certain aspects of Isabelle/ML to the outside world.
The Scala language (by Martin Odersky) is sufficiently close to ML in
order to model well-known prover concepts conveniently, but Scala also
runs on the JVM and can access existing Java libraries directly.  By
building more and more external system wrapping for Isabelle in Scala, we
eventually reach the point where we can integrate the prover seamlessly
into existing IDEs (say Netbeans).

To avoid getting side-tracked by IDE platform complexity, our current
experiments are focused on jEdit, which is a powerful editor framework
written in Java that can be easily extended by plugin modules.  Our
plugins are written again in Scala for our convenience, and to leverage
the Scala actor library for parallel and interactive programming.  Thanks
to the Isabelle/Scala layer, the Isabelle/jEdit implementation is very
small and simple.