Functional design and implementation of graphical user interfaces for theorem provers The design of theorem provers, especially in the LCF-prover family, has strongly profited from functional programming. 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.
Keywords for this software
References in zbMATH (referenced in 8 articles , 1 standard article )
Showing results 1 to 8 of 8.
- Gast, Holger: Engineering the prover interface (2012)
- Aspinall, David; Lüth, Christoph; Winterstein, Daniel: A framework for interactive proof (2007)
- Dixon, Lucas; Fleuriot, Jacques: A proof-centric approach to mathematical assistants (2006)
- Grabowski, Adam; Schwarzweller, Christoph: Translating mathematical vernacular into knowledge repositories (2006)
- Gunter, Elsa; Peled, Doron: Unit checking: symbolic model checking for a unit of code (2003)
- Autexier, Serge; Mossakowski, Till: Integrating HOL-CASL into the development graph manager MAYA (2002)
- Dosch, Walter; Magnussen, Sönke: The Lübeck transformation system: A transformation system for equational higher order algebraic specifications (2001)
- Lüth, C.; Wolff, B.: Functional design and implementation of graphical user interfaces for theorem provers (1999)