| Publication | Date of Publication | Type |
|---|
| On complexity of confluence and Church-Rosser proofs | 2026-05-12 | Paper |
On proving consistency of equational theories in bounded arithmetic
The Journal of Symbolic Logic | 2025-05-06 | Paper |
| 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
(available as arXiv preprint) | 2022-03-09 | Paper |
Cobham recursive set functions and weak set theories
Sets and Computations | 2020-12-02 | Paper |
Feasible set functions have small circuits
Computability | 2019-10-28 | Paper |
On transformations of constant depth propositional proofs
Annals of Pure and Applied Logic | 2019-07-10 | Paper |
Hyper natural deduction for Gödel logic -- a natural deduction system for parallel reasoning
Journal Of Logic And Computation | 2019-01-31 | Paper |
Hyper natural deduction
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
Deciding logics of linear Kripke frames with scattered end pieces
Soft Computing | 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
ACM Transactions on Computational Logic | 2017-07-13 | Paper |
Cobham recursive set functions
Annals of Pure and Applied Logic | 2016-01-12 | Paper |
Safe recursive set functions
Journal of Symbolic Logic | 2015-11-09 | Paper |
Separating intermediate predicate logics of well-founded and dually well-founded structures by monadic sentences
Journal Of Logic And Computation | 2015-07-15 | Paper |
Parity Games and Propositional Proofs
ACM Transactions on Computational Logic | 2014-07-17 | Paper |
Improved witnessing and local improvement principles for second-order bounded arithmetic
ACM Transactions on Computational Logic | 2014-04-16 | Paper |
Parity Games and Propositional Proofs
Mathematical Foundations of Computer Science 2013 | 2013-09-20 | Paper |
Corrected upper bounds for free-cut elimination
Theoretical Computer Science | 2011-10-10 | Paper |
On the computational complexity of cut-reduction
Annals of Pure and Applied Logic | 2011-08-26 | Paper |
| Characterising definable search problems in bounded arithmetic via proof notations | 2011-03-09 | Paper |
Polynomial local search in the polynomial hierarchy and witnessing in fragments of bounded arithmetic
Journal of Mathematical Logic | 2010-08-26 | Paper |
A Characterisation of Definable NP Search Problems in Peano Arithmetic
Logic, Language, Information and Computation | 2009-07-02 | Paper |
Continuous Fraïssé conjecture
Order | 2009-04-24 | Paper |
Propositional Logic for Circuit Classes
Computer Science Logic | 2009-03-05 | Paper |
Proofs, Programs and Abstract Complexity
Computer Science Logic | 2009-03-05 | Paper |
Linear Kripke frames and Gödel logics
Journal of Symbolic Logic | 2007-03-12 | Paper |
| Generalised dynamic ordinals -- universal measures for implicit computational complexity | 2006-10-17 | Paper |
Uniform Proof Complexity
Journal Of Logic And Computation | 2005-10-18 | Paper |
Separation results for the size of constant-depth propositional proofs
Annals of Pure and Applied Logic | 2005-09-22 | Paper |
An unexpected separation result in Linearly Bounded Arithmetic
MLQ | 2005-04-07 | Paper |
Preservation theorems and restricted consistency statements in bounded arithmetic
Annals of Pure and Applied Logic | 2004-08-06 | Paper |
Dynamic ordinal analysis
Archive for Mathematical Logic | 2003-09-16 | Paper |
A non-well-founded primitive recursive tree provably well-founded for co-r. e. sets
Archive for Mathematical Logic | 2003-09-16 | Paper |
| scientific article; zbMATH DE number 1980917 (Why is no real title available?) | 2003-09-15 | Paper |
| scientific article; zbMATH DE number 1948189 (Why is no real title available?) | 2003-07-10 | Paper |
Proving consistency of equational theories in bounded arithmetic
Journal of Symbolic Logic | 2003-05-29 | Paper |
Ordinal notations and well-orderings in bounded arithmetic
Annals of Pure and Applied Logic | 2003-03-16 | Paper |
Notations for exponentiation.
Theoretical Computer Science | 2003-01-21 | Paper |
Exact bounds for lengths of reductions in typed -calculus
The Journal of Symbolic Logic | 2001-12-06 | Paper |
Characterizing the elementary recursive functions by a fragment of Gödel's \(T\)
Archive for Mathematical Logic | 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
Annals of Pure and Applied Logic | 1999-11-15 | Paper |
A term rewriting characterization of the polytime functions and related complexity classes
Archive for Mathematical Logic | 1997-06-02 | Paper |
| scientific article; zbMATH DE number 963569 (Why is no real title available?) | 1997-01-09 | Paper |
