| A BOUND FOR DICKSON'S LEMMA | 1 | 0.38 | 2017 |
| Embedding classical in minimal implicational logic. | 0 | 0.34 | 2016 |
| Program extraction in exact real arithmetic. | 1 | 0.36 | 2015 |
| Minimal from Classical Proofs | 0 | 0.34 | 2013 |
| Program extraction from nested definitions | 1 | 0.35 | 2013 |
| Minlog: a tool for program extraction supporting algebras and coalgebras | 8 | 0.59 | 2011 |
| Realizability interpretation of proofs in constructive analysis | 7 | 0.51 | 2008 |
| Dialectica interpretation of well-founded induction. | 7 | 0.98 | 2008 |
| An arithmetic for polynomial-time computation | 7 | 0.46 | 2006 |
| Minlog | 1 | 0.36 | 2006 |
| Inverting monotone continuous functions in constructive analysis | 2 | 0.41 | 2006 |
| A Direct Proof of the Equivalence between Brouwer's Fan Theorem and König's Lemma with a Uniqueness Hypothesis | 9 | 0.79 | 2005 |
| An arithmetic for non-size-increasing polynomial-time computation | 5 | 0.46 | 2004 |
| Term rewriting for normalization by evaluation | 14 | 0.95 | 2003 |
| Refined program extraction from classical proofs | 34 | 2.45 | 2002 |
| Linear Ramified Higher Type Recursion and Parallel Complexity | 3 | 0.41 | 2001 |
| The Warshall Algorithm and Dickson's Lemma: Two Examples of Realistic Program Extraction | 16 | 1.48 | 2001 |
| A Syntactical Analysis Of Non-Size-Increasing Polynomial Time Computation | 0 | 0.34 | 2000 |
| Computer Science Logic, 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, Proceedings | 31 | 8.68 | 2000 |
| Higher type recursion, ramification and polynomial time | 39 | 1.98 | 2000 |
| A syntactical analysis of non-size-increasing polynomial time computation | 15 | 1.85 | 2000 |
| Terminiation of permutative conversions in intuitionistic Gentzen calculi | 15 | 4.24 | 1999 |
| Monotone Majorizable Functionals | 1 | 0.36 | 1999 |
| Finite notations for infinite terms | 3 | 0.43 | 1998 |
| Normalisation by Evaluation | 28 | 1.75 | 1998 |
| Strict Functionals for Termination Proofs | 29 | 2.22 | 1995 |
| The Greatest Common Divisor: A Case Study for Program Extraction from Classical Proofs | 5 | 1.17 | 1995 |
| Program Extraction from Classical Proofs | 19 | 2.72 | 1994 |
| An upper bound for reduction sequences in the typed λ-calculus | 3 | 0.47 | 1991 |
| An Inverse Of The Evaluation Functional For Typed Lambda-Calculus | 59 | 4.44 | 1991 |
| Ein einfaches Verfahren zur Normalisierung unendlicher Herleitungen | 2 | 1.00 | 1987 |
| On Bar Recursion of Types 0 and 1 | 7 | 1.12 | 1979 |
| Definierbare Funktionen im-Kalkül mit Typen. | 1 | 0.43 | 1975 |
