| Publication | Date of Publication | Type |
|---|
| Completeness of cyclic proofs for symbolic heaps with inductive definitions | 2024-04-19 | Paper |
| Cut elimination for propositional cyclic proof systems with fixed-point operators | 2023-12-20 | Paper |
| Decision Procedure for Entailment of Symbolic Heaps with Arrays | 2022-12-09 | Paper |
| Monotone recursive definition of predicates and its realizability interpretation | 2022-08-16 | Paper |
| A decidable fragment in separation logic with inductive predicates and arithmetic | 2022-08-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4989410 | 2021-05-25 | Paper |
| Type inference for bimorphic recursion | 2021-03-03 | Paper |
| Equivalence of inductive definitions and cyclic proofs under arithmetic | 2021-01-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5227521 | 2019-08-06 | Paper |
| Completeness and expressiveness of pointer program verification by separation logic | 2019-05-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 |
| Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System | 2017-05-19 | Paper |
| Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic | 2016-12-21 | Paper |
| Completeness for recursive procedures in separation logic | 2016-05-02 | Paper |
| Separation logic with monadic inductive definitions and implicit existentials | 2016-01-08 | Paper |
| On isomorphisms of intersection types | 2015-09-17 | Paper |
| Static analysis of multi-staged programs via unstaging translation | 2014-04-10 | Paper |
| A behavioural model for Klop's calculus | 2013-12-04 | Paper |
| Games with sequential backtracking and complete game semantics for subclassical logics | 2013-06-28 | Paper |
| Call-by-value and call-by-name dual calculi with inductive and coinductive types | 2013-04-09 | Paper |
| Non-commutative infinitary Peano arithmetic | 2012-09-18 | Paper |
| Internal models of system F for decompilation | 2012-06-25 | Paper |
| Type checking and typability in domain-free lambda calculi | 2012-01-04 | Paper |
| Inhabitation of polymorphic and existential types | 2011-08-26 | Paper |
| Internal normalization, compilation and decompilation for System \({\mathcal F}_{\beta\eta}\) | 2010-05-04 | Paper |
| Non-Commutative First-Order Sequent Calculus | 2009-11-12 | Paper |
| Dual Calculus with Inductive and Coinductive Types | 2009-06-30 | Paper |
| Simple Saturated Sets for Disjunction and Second-Order Existential Quantification | 2009-03-10 | Paper |
| Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence | 2008-11-20 | Paper |
| On Isomorphisms of Intersection Types | 2008-11-20 | Paper |
| Positive Arithmetic Without Exchange Is a Subclassical Logic | 2008-05-15 | Paper |
| Strong normalization of classical natural deduction with disjunctions | 2008-04-24 | Paper |
| Types for Hereditary Head Normalizing Terms | 2008-04-11 | Paper |
| The Maximum Length of Mu-Reduction in Lambda Mu-Calculus | 2008-01-02 | Paper |
| A simple proof of second-order strong normalization with permutative conversions | 2005-09-22 | Paper |
| Strong normalization proof with CPS-translation for second order classical natural deduction | 2005-02-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4936128 | 2000-01-24 | Paper |
| The function \(\lfloor a/m\rfloor\) in sharply bounded arithmetic | 1998-05-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5688910 | 1997-04-21 | Paper |
| TWO REALIZABILITY INTERPRETATIONS OF MONOTONE INDUCTIVE DEFINITIONS | 1994-12-12 | Paper |
| Realizability interpretation of generalized inductive definitions | 1994-12-05 | Paper |
| Realizability interpretation of coinductive definitions and program synthesis with streams | 1994-11-29 | Paper |
| Uniqueness of normal proofs of minimal formulas | 1994-07-07 | Paper |
| Program synthesis using realizability | 1992-06-28 | Paper |
| The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions | N/A | Paper |
