

The Refute Regex Tool

The Refute Regex Translation Tool automatically enumerates translations represented by regular expressions from the PISIMPLEcalculus to the CHSIMPLEcalculus and tries to invalidate them from being convergence equivalent. The tool (and further information) can be found on
via this URL

The Refute Pi Translation Tool

The Refute Pi Translation Tool automatically enumerates translations from the picalculus to the CHcalculus and tries to invalidate them from being convergence equivalent.
The tool (and further information) can be found on
via this URL

The LRSX Tool

The LRSX Tool implements a procedure to automatically prove correctness of program transformations for
higherorder program calculi with recursive and shared bindings (i.e. socalled letrecexpressions).
The tool (and further information) can be found on
this webpage

The LRSX Unification Tool

The LRSX Unification Tool implements a new algorithm for unification of metaexpressions
in lambda calculi with recursive and shared bindings (i.e. socalled letrecexpressions).
The tool (and further information) can be found on this webpage.

cycsrs  Proving Termination of Cycle Rewriting

The tool cycsrs combines several techniques and tools to prove termination
of cycle rewriting. It participated in the Termination Competition 2015
and in the Termination and Complexity Competition 2016.
The tool and a webinterface can be found on
this webpage.

SHFSTM  Software Transactional Memory

An alternative implementation of Software Transactional Memory in Haskell can be found
on this webpage.

GBC  GrammarBased Compression

Several algorithms on grammarcompressed matrices, grammarcompressed strings and grammarcompressed terms can be found
here.

Allen's Interval Logic

Allen's interval logic is a calculus for temporal logic.
A webinterface can be found here.
A Haskell implementation as a Cabalpackage is
allen0.1.0.0.tar.gz.

HasFuse

The (somewhat outdated) webpage of HasFuse (Haskell with FUNDIObased sideeffects)
can be found here.
