My research interests are concerned with automated reasoning, logic (in particular proof theory), programming languages (in particular term rewrite systems) and resource analysis. My achievements can be classified into the following two strands: automated resource analysis and structural proof theory.

#### automated resource analysis

Static resource analyis of programs employs formal methods to statically analyse software for the resource consumption. Resources of interest are typically time or memory consumption, but do also encompass heath dissipation or energy consumption. My main expertise in this area is concerned with a transformational approach. Given a source program and a resource of interest, we transform the program into an abstract program (for example a term rewrite system or an integer transition system) and perform our analysis on this intermediate representation. The transformation is understood to be complexity reflecting. Employing this idea my group build the award-winning tool TcT.

#### structural proof theory

Proof theory is one of the central pillars of mathematical logic. Proof-theoretic investigations in Hilbert's tradition were mainly concerned with questions of provability. However, in order to study provability a more refined study of the structure of proofs is needed. This observation led to investigations into structural proof theory. Structural proof theory plays a crucial role in the foundations of programming language. My interest in structural proof theory encompasses Herbrand's Theorem, Hilbert's epsilon calculus, Curry-Howard correspondence and deep inference.