| Publication | Date of Publication | Type |
|---|
| Termination of rewriting on reversible Boolean circuits as a free 3-category problem | 2025-01-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4992894 | 2021-06-10 | Paper |
| Equivalence of inductive definitions and cyclic proofs under arithmetic | 2021-01-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5227521 | 2019-08-06 | Paper |
| An analysis of the Podelski-Rybalchenko termination theorem via bar recursion | 2019-07-29 | Paper |
| Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs | 2018-10-23 | Paper |
| Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic | 2017-12-10 | Paper |
| Non-monotonic pre-fix points and learning | 2017-11-10 | Paper |
| Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness | 2017-08-31 | Paper |
| Ramsey's theorem for pairs and \(k\) colors as a sub-classical principle of arithmetic | 2017-08-03 | Paper |
| Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System | 2017-05-19 | Paper |
| Ramsey theorem for pairs as a classical principle in intuitionistic arithmetic | 2017-03-13 | Paper |
| Realizability and strong normalization for a Curry-Howard interpretation of HA + EM1 | 2017-02-02 | Paper |
| An intuitionistic version of Ramsey's theorem and its use in program termination | 2015-09-29 | Paper |
| Interactive realizers: a new approach to program extraction from nonconstructive proofs | 2015-09-17 | Paper |
| Ramsey theorem as an intuitionistic property of well founded relations | 2014-07-24 | Paper |
| A new use of Friedman's translation: interactive realizability | 2014-06-24 | Paper |
| Knowledge spaces and the completeness of learning strategies | 2014-03-24 | Paper |
| Games with sequential backtracking and complete game semantics for subclassical logics | 2013-06-28 | Paper |
| Knowledge spaces and the completeness of learning strategies | 2012-11-22 | Paper |
| Non-commutative infinitary Peano arithmetic | 2012-09-18 | Paper |
| Internal models of system F for decompilation | 2012-06-25 | Paper |
| Games with 1-backtracking | 2011-08-26 | Paper |
| Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\) | 2010-09-21 | Paper |
| Internal normalization, compilation and decompilation for System \({\mathcal F}_{\beta\eta}\) | 2010-05-04 | Paper |
| Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1 | 2009-07-07 | Paper |
| Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves | 2009-03-10 | Paper |
| Toward the interpretation of non-constructive reasoning as non-monotonic learning | 2009-03-02 | Paper |
| A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract) | 2008-11-20 | Paper |
| Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca | 2008-06-24 | Paper |
| Positive Arithmetic Without Exchange Is a Subclassical Logic | 2008-05-15 | Paper |
| A sequent calculus for limit computable mathematics | 2008-04-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5456617 | 2008-04-14 | Paper |
| Some intuitionistic equivalents of classical principles for degree 2 formulas | 2006-04-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3024822 | 2005-07-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3024824 | 2005-07-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3024898 | 2005-07-04 | Paper |
| Classical logic as limit completion | 2005-03-14 | Paper |
| Krivine's intuitionistic proof of classical completeness (for countable languages) | 2004-11-22 | Paper |
| Building continuous webbed models for system F | 2004-08-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4472544 | 2004-08-04 | Paper |
| A generalization of a conservativity theorem for classical versus intuitionistic arithmetic | 2004-03-15 | Paper |
| βη-complete models for System F | 2004-02-08 | Paper |
| A full continuous model of polymorphism | 2003-01-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4513574 | 2001-02-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4247298 | 2000-07-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4490745 | 2000-07-20 | Paper |
| Approximating classical theorems | 2000-07-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4699354 | 2000-05-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4263862 | 1999-11-21 | Paper |
| A parallel game semantics for linear logic | 1999-10-28 | Paper |
| Intuitionistic completeness for first order classical logic | 1999-06-29 | Paper |
| On the computational content of the axiom of choice | 1999-06-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4364394 | 1998-04-15 | Paper |
| The simply typed theory of \(\beta\)-conversion has no maximum extension | 1998-04-02 | Paper |
| A constructive valuation semantics for classical logic | 1998-03-12 | Paper |
| Pruning simply typed -terms | 1997-06-03 | Paper |
| A symmetric lambda calculus for classical program extraction | 1997-01-05 | Paper |
| Proof-irrelevance out of excluded-middle and choice in the calculus of constructions | 1996-12-16 | Paper |
| A strong normalization result for classical logic | 1996-03-05 | Paper |
| An application of PER models to program extraction | 1994-03-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4281464 | 1994-03-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3970572 | 1992-06-25 | Paper |
| Retractions of dI-domains as a model for Type:Type | 1991-01-01 | Paper |
| Equalization of finite flowers | 1988-01-01 | Paper |
| Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem | N/A | Paper |
