Computation with Bounded Resources
Research Group

Computation with Bounded Resources

The theory of computability as developed at the beginning of the last century lies at the very heart of computer science. Computations, where the resources are limited, can be conceived as investigations into computational complexity theory. On the other hand computations with bounded resources have also been intensively studied in the area of program analysis, as program analysis offers techniques for predicting the behaviour of programs.

While traditionally these two conceptions of computation with limited resources are studied in quite separate communities, our research aims to unify the approaches to get the best of both worlds. The methodology used for this are investigations into the logical foundations of the nature of computation (with bounded resources) and (automated) resource analysis of programs.

The Past

Initially our research was mainly concerned with complexity analysis of first-order term rewrite systems. Rewriting is a simple, but powerful abstract model of computation that underlies much of declarative programming. Our main theoretical contributions were the modernisation of derivational complexity analysis and the development of automated runtime complexity of term rewrite systems. Our work has had a considerable impact within the rewriting community such that the important area of complexity of rewriting has been thoroughly revived.

The Present

Our current research encompasses investigations into structural proof theory and in particular deep inference, in order to better extract computational content from proofs. These theoretical tools are employed to provide automated tools for the re source analysis of imperative and declarative programming languages, like C, Haskell, Java or Prolog. To this avail we employ complexity reflecting program transformatoons to represent the source program within an intermediary representation (rewrite systems in various guises: term rewrite systems, higher-order rewrite systems, graph rewrite systems, interaction nets, integer transition systems, etc. ).

Our resource analyser, the TcT is open source and freely available. As repeatedly verified by the annual termination competition (TERMCOMP) and at the FLOC Olympic Games 2014, TcT is the most powerful complexity analyser for term rewrite systems and state of the art for higher-order functional programs.

The Future

Very recent work on time and space complexity of interaction net systems may provide the logical foundation of a more adequate model of computation for parallel and distributed computation and give rise to resource aware programming.