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