• 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.

  Homepage System description
• 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.

  Homepage
• GUBS

  A constraint solver for polynomial inequalities.

  Homepage GitHub System description
• 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.

  Homepage GitHub System description
• Higher Order Sized-Type Analysis (HOSA)

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

  Homepage GitHub System description
• Implicit Computational Complexity Tool (ICCT)

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

  Homepage System description
• 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.

  Homepage GitHub System description

Libraries

• Haskell Applicative Rewriting Library

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

  GitHub
• Haskell Term Rewriting Library

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

  Homepage GitHub Hackage
• 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.

  Homepage GitHub