[Club2] 8.03: 14.30 und 9.03: 11:30 (Turing)

[Norbert Schirmer]

Diese Woche:

Do: 08.03.2007, 14:30 (Zimmer Turing: 00.09.055)

David Aspinall, Informatics, Edinburgh
Christoph Lüth, DFKI, Bremen

                  The Future of Proof Engineering
                        with Proof General


Future work on Proof General is centred around the challenge of Proof
Engineering, which we see as being necessary to take interactive
theorem proving to the next level.  Proof Engineering, like Software
Engineering, considers the lifecycle of large proof developments.  It
will provide facilities for the construction, maintenance, and
comprehension of large proofs.  We want to provide foundations and
tools to support Proof Engineering at a generic level, within the
Proof General Kit framework.

We will introduce some of the research problems and early solution
ideas for our new programme and explain how they relate to Isabelle,
which we hope will be one of the first theorem provers to benefit.  We
mention some of the desirable modifications and extensions to Isabelle
for supporting Proof Engineering.

The talk will conclude with a demonstration of the new Proof General
Eclipse system which will be the flagship tool for Proof Engineering.

#########################################################

Fr: 09.03.2007, 11:30 (Zimmer Turing: 00.09.055)

Cezary Kaliszyk:

Web Interface for Proof Assistants and the Development of a Wiki for
Formalized Mathematics

We present an architecture for creating responsive web interfaces
for proof assistants, and discuss using it in a a wiki environment.
The architecture combines the functionality of local prover interfaces
with current web development technologies, to create an interface that
is available completely within a web browser, but resembles and behaves
like a local one. We will discuss security, availability and efficiency
issues of the proposed architecture. We will demonstrate an  
implementation
that uses basic PGIP commands to communicate with the Isabelle proof
assistant and present some ideas on how to take advantage of more of the
PGIP protocol.


     Norbert