Software

David Sabel

The Refute Regex Tool

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

The Refute Pi Translation Tool

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

The LRSX Tool

The LRSX Tool implements a procedure to automatically prove correctness of program transformations for higher-order program calculi with recursive and shared bindings (i.e. so-called letrec-expressions). The newest version of the tool (and further information) can be found on this git repository, also archived on zenodo.org with DOI 10.5281/zenodo.17242132.
Older versions with other examples are available here: [Version 0.4.2 | Version 0.6.0 | Version 0.6.1]

The LRSX Unification Tool

The LRSX Unification Tool implements a new algorithm for unification of meta-expressions in lambda calculi with recursive and shared bindings (i.e. so-called letrec-expressions). 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 can be found on this webpage.

SHFSTM - Software Transactional Memory

An alternative implementation of Software Transactional Memory in Haskell can be found in this git repository.

GBC - Grammar-Based Compression

Several algorithms on grammar-compressed matrices, grammar-compressed strings and grammar-compressed terms can be found here.

Allen's Interval Logic

Allen's interval logic is a calculus for temporal logic. A Haskell implementation as a Cabal-package is available from this git repository.

HasFuse

The (somewhat outdated) webpage of HasFuse (Haskell with FUNDIO-based side-effects) can be found here.