Theoretical Computer Science

Theoretical Computer Science Group

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 firstly concerned with the fully automated resource analysis of programs. Our work has had a considerable impact in the resource analysis of (first-order) term rewrite systems, as well as (higher-order) functional programming. Further, we provided novel insights into structural proof theory and in particular deep inference, in order to better extract computational content from proofs. One example of the use of fundamental theoretical studies in practical application areas was recent work on time and space complexity analysis of interaction net systems.

The Present

Our resource analyser, the Tyrolean Complexity Tool (TcT) is open source and freely available. Our current research aims to unify existing approaches into a uniform framework for resource analysis, that allows the automated assessment of the resource usage for a variety of input programs, parameterised with respect to the considered resource metric. We envision an analysis geared towards modern programming practise, with its desire to mix different programming paradigms.

The Future

For the future, we envision the consolidation of our work on resource analysis, as well as the exploration of these theoretical results in application areas like (i) security and reliability of software, (ii) probabilistic programming and (iii) resource-aware programming. Further, we aim to investigate the use of resource analysis in the context of inductive programming.