Coding projects
- CTRL, a constrained rewriting tool
- WANDA, a higher order termination tool
- Terms Library, a library for higher order term rewrite systems in applicative form
Ctrl
One of the targets of the constrained rewriting and SMT project was the development of a tool for rewriting and analysis of constrained term rewriting systems. This tool, Ctrl, is available at http://cl-informatik.uibk.ac.at/software/ctrl/, en is documented in a conference paper at LPAR 2015.
Wanda
Although writing code was not the core of my PhD research, syntactic termination methods are usually best demonstrated with a tool that implements them. To this end, I developed WANDA, a termination tool which implements new higher-order termination techniques (focused, for obvious reasons, on those techniques to which I contributed).
WANDA has been developed for participation in the annual termination competition. Apart from the competition's xml-format, a number of other formats are accepted, as explained in the README.txt file in the downloads.
WANDA can be downloaded from WANDA's page at sourceforge.
Underlying theory: WANDA v2.0 (the version available from sourceforge) is primarily based on my PhD thesis. Here it is described how WANDA obtains her results. To some extent, the thesis might be seen as WANDA's documentation.
Terms Library
Having a convenient C++ library to work with terms has more purpose than just a termination tool. Therefore I kept the terms library as general as possible. The program itself doesn't do anything particularly exciting, but the code may be useful for more advanced applications.