Sciweavers

FASE
2000
Springer

More About TAS and IsaWin - Tools for Formal Program Development

14 years 1 months ago
More About TAS and IsaWin - Tools for Formal Program Development
We present a family of tools for program development and verification, comprising the transformation system TAS and the theorem proving interface IsaWin. Both are based on the theorem prover Isabelle [8], which is used as a generic logical framework here. A graphical user interface, based on the principle of direct manipulation, allows the user to interact with the tool without having to concern himself with the details of the representation within the theorem prover, leaving him to concentrate on the main design decisions of program development or theorem proving.
Christoph Lüth, Burkhart Wolff
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where FASE
Authors Christoph Lüth, Burkhart Wolff
Comments (0)