Software
The following gives a list of 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.
- EasyCrypt
EasyCrypt is an interactive framework for verifying the security of cryptographic constructions in the computational model. I have contributed to the design of the expectation Hoare Logic (eHL), implemented as eHoare within EasyCrypt.
- 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.
- 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.
Libraries
- Haskell Applicative Rewriting Library
This library extends the Haskell term-rewriting library by providing functionality for applicative rewrite systems.
- 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.