TAS and IsaWin home page.

Welcome to the TAS and IsaWin home page!


TAS and IsaWin are tools for formal program development and theorem proving developed at the University of Bremen and Albert-Ludwigs-Universität, Freiburg.

TAS is a transformation system based on the theorem prover Isabelle. It features:

In particular, genericity means it can be used for any formal method which offers a notion of correctness-preserving refinement, or in fact any transitive-reflexive transformation relation, which is encoded into Isabelle. We have investigated instantiations for classical program transformations (in the style of systems like KIDS using plain higher-order logic), for the specification language Z (using the HOL-Z encoding), the process calculus CSP (using the HOL-CSP encoding), and the algebraic specification language CASL (using the HOL-CASL encoding).

IsaWin is a graphical user interface for the theorem prover Isabelle. It offers the user a more abstract view on Isabelle then its ususal command-line based interface.

Both systems are built using sml_tk, an encapsulation of the user interface description language and library Tcl/Tk into Standard ML (SML). Building on this, we provide a Generic Interface Toolkit which can be used to quickly built graphical user interfaces like TAS and IsaWin.

Demos and Screenshots

Here is a full screenshot of TAS and IsaWin, but you to get a taste of TAS and IsaWin you can download a demo version below. Note that these are preliminary demo versions with a deliberately limited functionality. The demos are plug&play without a complicated configuration procedure. To run them, unpack the file tas_demo.tar.gz. This will produce a directory tas_demo. Go into this directory, and call bin/TAS_demo. The file README (in tas_demo) contains further information.

TAS and IsaWin are still in a prototypical stage, so we unfortunately at this point we can only make the demo versions above available to the public. A full working version should be available by the start of the next year.

Papers and Documentation

Here are a couple of papers about TAS and IsaWin. More can be found here and here. On a more historic note, the system YATS, the ancestor of TAS from which it inherits its design and many concepts, is described in:


TAS, IsaWin and the Generic Interface Toolkit are developed jointly by Christoph Lüth at the University of Bremen and Burkhart Wolff at the Albert-Ludwigs-Universität Freiburg. The development was initially funded by the UniForM project.
Christoph Lüth. Last modified: Tue Dec 2 16:09:09 CET 2003