| Publication | Date of Publication | Type |
|---|
| Verification of bitcoin script in Agda using weakest preconditions for access control | 2024-08-01 | Paper |
| On proving consistency of equational theories in Bounded Arithmetic | 2022-03-09 | Paper |
| COBHAM RECURSIVE SET FUNCTIONS AND WEAK SET THEORIES | 2020-12-02 | Paper |
| Feasible set functions have small circuits | 2019-10-28 | Paper |
| On transformations of constant depth propositional proofs | 2019-07-10 | Paper |
| Hyper Natural Deduction for Gödel Logic—A natural deduction system for parallel reasoning | 2019-01-31 | Paper |
| Hyper Natural Deduction | 2018-04-23 | Paper |
| Deciding logics of linear Kripke frames with scattered end pieces | 2018-02-23 | Paper |
| Total search problems in bounded arithmetic and improved witnessing | 2017-12-20 | Paper |
| The NP Search Problems of Frege and Extended Frege Proofs | 2017-07-13 | Paper |
| Cobham recursive set functions | 2016-01-12 | Paper |
| SAFE RECURSIVE SET FUNCTIONS | 2015-11-09 | Paper |
| Separating intermediate predicate logics of well-founded and dually well-founded structures by monadic sentences | 2015-07-15 | Paper |
| Parity Games and Propositional Proofs | 2014-07-17 | Paper |
| Improved witnessing and local improvement principles for second-order bounded arithmetic | 2014-04-16 | Paper |
| Parity Games and Propositional Proofs | 2013-09-20 | Paper |
| Corrected upper bounds for free-cut elimination | 2011-10-10 | Paper |
| On the computational complexity of cut-reduction | 2011-08-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3081638 | 2011-03-09 | Paper |
| POLYNOMIAL LOCAL SEARCH IN THE POLYNOMIAL HIERARCHY AND WITNESSING IN FRAGMENTS OF BOUNDED ARITHMETIC | 2010-08-26 | Paper |
| A Characterisation of Definable NP Search Problems in Peano Arithmetic | 2009-07-02 | Paper |
| Continuous Fraïssé conjecture | 2009-04-24 | Paper |
| Proofs, Programs and Abstract Complexity | 2009-03-05 | Paper |
| Propositional Logic for Circuit Classes | 2009-03-05 | Paper |
| Linear Kripke frames and Gödel logics | 2007-03-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5494228 | 2006-10-17 | Paper |
| Uniform Proof Complexity | 2005-10-18 | Paper |
| Separation results for the size of constant-depth propositional proofs | 2005-09-22 | Paper |
| An unexpected separation result in Linearly Bounded Arithmetic | 2005-04-07 | Paper |
| Preservation theorems and restricted consistency statements in bounded arithmetic | 2004-08-06 | Paper |
| Dynamic ordinal analysis | 2003-09-16 | Paper |
| A non-well-founded primitive recursive tree provably well-founded for co-r. e. sets | 2003-09-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4428291 | 2003-09-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4411850 | 2003-07-10 | Paper |
| Proving consistency of equational theories in bounded arithmetic | 2003-05-29 | Paper |
| Ordinal notations and well-orderings in bounded arithmetic | 2003-03-16 | Paper |
| Notations for exponentiation. | 2003-01-21 | Paper |
| Exact bounds for lengths of reductions in typed \(\lambda\)-calculus | 2001-12-06 | Paper |
| Characterizing the elementary recursive functions by a fragment of Gödel's \(T\) | 2001-07-26 | Paper |
| Analyzing Gödel's T Via Expanded Head Reduction Trees | 2001-07-16 | Paper |
| Applications of cut-free infinitary derivations to generalized recursion theory | 1999-11-15 | Paper |
| A term rewriting characterization of the polytime functions and related complexity classes | 1997-06-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5691043 | 1997-01-09 | Paper |
