Abstract:

Functional Design and Implementation of Graphical User Interfaces for Theorem Provers

Christoph Lüth and Burkhart Wolff


This paper attempts to develop a metaphor suited to visualize the LCF-style prover design, and a methodology 
for the implementation of graphical user interfaces for these provers and encapsulations of formal methods. 
In this problem domain, particular attention has to be paid to the need to construct a variety of objects, keep 
track of their interdependencies and provide support for their reconstruction as a consequence of changes. 
We present a prototypical implementation of a generic and open interface system architecture, and show 
how it can be instantiated to an interface for Isabelle, called IsaWin, as well as to a tailored tool for 
transformational program development, called TAS.