home > software > index


The following gives a short list of most important software projects I'm involved in.

  • IsaFoR/CeTA

    CeTA is a tool that certifies proofs of non-functional properties of rewrite systems, such as termination, confluence, and complexity, provided by automated tools that support the certification problem format format. It mainly consists of two parts.

    • An Isabelle/HOL formalization of some current termination techniques, as part of the library IsaFoR.

    • An automatically generated Haskell program (using the code-generation feature of Isabelle) to certify proofs.

    I have contributed the formalisation of dependency tuples.

  • Expected Cost Analysis for Imperative Programs (eco-imp)

    This tool implements a fully automated analysis on the expected resource consumption of imperative programs with sampling instructions.

  • GUBS

    A constraint solver for polynomial inequalities.

  • Higher Order Complexity Analysis (HOCA)

    HOCA is an abbreviation for Higher-Order Complexity Analysis, and is meant as a laboratory for the automated complexity analysis of higher-order functional programs. HOCA translates a pure subset of OCaml to term rewrite systems, in a complexity reflecting manner. Complexity certificates such as the ones obtained by first order provers like TCT, can be relayed (asymptotically) back to the OCaml program.

  • Higher Order Sized-Type Analysis (HOSA)

    HOSA implements complexity analysis of higher-order functional programs via sized-types.

  • Implicit Computational Complexity Tool (ICCT)

    A tool to analyse the implicit computational complexity of programs, expressed as term rewrite systems.

  • Tyrolean Complexity Tool (TCT)

    The Tyrolean Complexity Tool is a tool for automatically proving polynomial upper bounds on the derivational complexity and runtime complexity of term rewriting systems.


  • Haskell Applicative Rewriting Library

    This library extends the Haskell term-rewriting library by providing functionality for applicative rewrite systems.

  • Haskell Term Rewriting Library

    This library provides basic data types and functionality for first-order term rewriting.

  • QLogic

    This is a Haskell library for dealing with propositional logic. In particular, it provides the following features:

    • Translation of diophantine constraints to propositional formulas
    • Translation of common arithmetical functions over Integers and Naturals to propositional formulas
    • A general interface to SAT-solvers, including efficient translation of arbitrary formulas to CNF.

    This library underlies the Tyrolean Complexity Tool, Version 2, it has been deprecated in favor of SLogic.