| Relativizing small complexity classes and their theories. | 4 | 0.44 | 2016 |
| A compiled implementation of normalisation by evaluation* | 10 | 0.78 | 2012 |
| Resource aware ML | 9 | 0.48 | 2012 |
| Multivariate Amortized Resource Analysis | 3 | 0.38 | 2011 |
| On the computational complexity of cut-reduction | 3 | 0.50 | 2010 |
| Normalization by Evaluation. | 0 | 0.34 | 2008 |
| Parameter-free polymorphic types | 1 | 0.36 | 2008 |
| Normalization by Evaluation for Martin-Löf Type Theory with One Universe | 7 | 0.58 | 2007 |
| Propositional logic for circuit classes | 1 | 0.63 | 2007 |
| A finite semantics of simply-typed lambda terms for infinite runs of automata | 21 | 1.04 | 2007 |
| The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable | 24 | 1.35 | 2005 |
| Induction and inductive definitions in fragments of second order arithmetic | 2 | 0.49 | 2005 |
| Continuous normalization for the lambda-calculus and Gödel’s T | 3 | 0.47 | 2005 |
| An arithmetic for non-size-increasing polynomial-time computation | 5 | 0.46 | 2004 |
| Operational aspects of untyped Normalisation by Evaluation | 10 | 0.74 | 2004 |
| An elementary fragment of second-order lambda calculus | 2 | 0.46 | 2002 |
| Linear Ramified Higher Type Recursion and Parallel Complexity | 3 | 0.41 | 2001 |
| A Syntactical Analysis Of Non-Size-Increasing Polynomial Time Computation | 0 | 0.34 | 2000 |
| A syntactical analysis of non-size-increasing polynomial time computation | 15 | 1.85 | 2000 |
