| Publication | Date of Publication | Type |
|---|
| Univalent monoidal categories | 2024-11-26 | Paper |
| Formalizing Monoidal Categories and Actions for Syntax with Binders | 2023-07-30 | Paper |
| Univalent Monoidal Categories | 2022-12-06 | Paper |
| Martin Hofmann's Case for Non-Strictly Positive Data Types | 2022-07-21 | Paper |
| Implementing a Category-Theoretic Framework for Typed Abstract Syntax | 2021-12-13 | Paper |
| A coinductive approach to proof search through typed lambda-calculi | 2021-09-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4995381 | 2021-06-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4992896 | 2021-06-10 | Paper |
| Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic | 2020-07-31 | Paper |
| Certification of breadth-first algorithms by extraction | 2020-05-05 | Paper |
| Decidability of Several Concepts of Finiteness for Simple Types | 2020-01-24 | Paper |
| Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search | 2019-10-09 | Paper |
| From signatures to monads in \textsf{UniMath} | 2019-08-21 | Paper |
| Heterogeneous Substitution Systems Revisited | 2018-08-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2957696 | 2017-01-27 | Paper |
| A Coinductive Approach to Proof Search through Typed Lambda-Calculi | 2016-02-13 | Paper |
| Monadic translation of classical sequent calculus | 2014-04-16 | Paper |
| Substitution in non-wellfounded syntax with variable binding | 2013-08-23 | Paper |
| Permutations in Coinductive Graph Representation | 2012-09-20 | Paper |
| Verification of the Schorr-Waite Algorithm – From Trees to Graphs | 2011-05-27 | Paper |
| Map fusion for nested datatypes in intensional type theory | 2011-02-21 | Paper |
| An induction principle for nested datatypes in intensional type theory | 2009-10-28 | Paper |
| Monadic Translation of Intuitionistic Sequent Calculus | 2009-07-02 | Paper |
| Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi | 2009-06-30 | Paper |
| A Datastructure for Iterated Powers | 2009-04-02 | Paper |
| Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi | 2009-03-10 | Paper |
| Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening | 2008-08-28 | Paper |
| Recursion on Nested Datatypes in Dependent Type Theory | 2008-06-19 | Paper |
| Verification of the Redecoration Algorithm for Triangular Matrices | 2008-06-03 | Paper |
| Stabilization -- an alternative to double-negation translation for classical natural deduction | 2006-07-03 | Paper |
| Computer Science Logic | 2005-08-22 | Paper |
| Non-strictly positive fixed points for classical natural deduction | 2005-04-21 | Paper |
| Iteration and coiteration schemes for higher-order and nested datatypes | 2005-04-06 | Paper |
| Substitution in non-wellfounded syntax with variable binding | 2005-01-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4436032 | 2003-11-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4435457 | 2003-11-12 | Paper |
| Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\) | 2003-09-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4417851 | 2003-07-30 | Paper |
| Tarski's fixed-point theorem and lambda calculi with monotone inductive types | 2003-04-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4783334 | 2002-12-04 | Paper |
| A locally trivial quantum Hopf bundle | 2002-10-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2778830 | 2002-03-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2723897 | 2001-07-08 | Paper |
| Monotone (co)inductive types and positive fixed-point types | 2000-07-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4263804 | 2000-03-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4720069 | 2000-01-09 | Paper |
