Linear Ramified Higher Type Recursion and Parallel Complexity. - Klaus Aehlig; Jan Johannsen; Helmut Schwichtenberg; Sebastiaan Terwijn (Proof Theory in Computer Science, 2001)

On Continuous Normalization. - Klaus Aehlig; Felix Joachimski (CSL, 2002)

A syntactical analysis of non-size-increasing polynomial time computation. - Klaus Aehlig; Helmut Schwichtenberg (ACM Trans. Comput. Log., 2002)

Operational aspects of untyped Normalisation by Evaluation. - Klaus Aehlig; Felix Joachimski (Math. Struct. Comput. Sci., 2004)

An arithmetic for non-size-increasing polynomial-time computation. - Klaus Aehlig; Ulrich Berger 001; Martin Hofmann 001; Helmut Schwichtenberg (Theor. Comput. Sci., 2004)

Safety Is not a Restriction at Level 2 for String Languages. - Klaus Aehlig; Jolie G. de Miranda; C.-H. Luke Ong (FoSSaCS, 2005)

The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable. - Klaus Aehlig; Jolie G. de Miranda; C.-H. Luke Ong (TLCA, 2005)

Continuous normalization for the lambda-calculus and Gödel's. - Klaus Aehlig; Felix Joachimski (Ann. Pure Appl. Log., 2005)

Induction and inductive definitions in fragments of second order arithmetic. - Klaus Aehlig (J. Symb. Log., 2005)

An elementary fragment of second-order lambda calculus. - Klaus Aehlig; Jan Johannsen (ACM Trans. Comput. Log., 2005)

Propositional Logic for Circuit Classes. - Klaus Aehlig; Arnold Beckmann (CSL, 2007)

Normalization by Evaluation for Martin-Löf Type Theory with One Universe. - Andreas Abel 001; Klaus Aehlig; Peter Dybjer (MFPS, 2007)

A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata. - Klaus Aehlig (Log. Methods Comput. Sci., 2007)

A Compiled Implementation of Normalization by Evaluation. - Klaus Aehlig; Florian Haftmann; Tobias Nipkow (TPHOLs, 2008)

Normalization by Evaluation. - Klaus Aehlig; Tobias Nipkow (Arch. Formal Proofs, 2008)

Parameter-free polymorphic types. - Klaus Aehlig (Ann. Pure Appl. Log., 2008)

On the computational complexity of cut-reduction. - Klaus Aehlig; Arnold Beckmann (Ann. Pure Appl. Log., 2010)

Resource Aware ML. - Jan Hoffmann 002; Klaus Aehlig; Martin Hofmann 001 (CAV, 2012)

A compiled implementation of normalisation by evaluation. - Klaus Aehlig; Florian Haftmann; Tobias Nipkow (J. Funct. Program., 2012)

Multivariate amortized resource analysis. - Jan Hoffmann 002; Klaus Aehlig; Martin Hofmann 001 (ACM Trans. Program. Lang. Syst., 2012)

Relativizing small complexity classes and their theories. - Klaus Aehlig; Stephen A. Cook; Phuong Nguyen 001 (Comput. Complex., 2016)