| 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
Annals of Pure and Applied Logic | 2021-09-30 | Paper |
| Confluence for classical logic through the distinction between values and computations | 2021-06-24 | Paper |
Confluence for classical logic through the distinction between values and computations
(available as arXiv preprint) | 2021-06-24 | Paper |
| A coinductive approach to proof search | 2021-06-10 | Paper |
A coinductive approach to proof search
(available as arXiv preprint) | 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
Fundamenta Informaticae | 2020-01-24 | Paper |
Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
Mathematical Structures in Computer Science | 2019-10-09 | Paper |
From signatures to monads in \textsf{UniMath}
Journal of Automated Reasoning | 2019-08-21 | Paper |
Heterogeneous substitution systems revisited
(available as arXiv preprint) | 2018-08-13 | Paper |
| Verification of redecoration for infinite triangular matrices using coinduction | 2017-01-27 | Paper |
A Coinductive Approach to Proof Search through Typed Lambda-Calculi
(available as arXiv preprint) | 2016-02-13 | Paper |
Monadic translation of classical sequent calculus
Mathematical Structures in Computer Science | 2014-04-16 | Paper |
| Substitution in non-wellfounded syntax with variable binding | 2013-08-23 | Paper |
Permutations in Coinductive Graph Representation
Coalgebraic Methods in Computer Science | 2012-09-20 | Paper |
Verification of the Schorr-Waite algorithm -- from trees to graphs
Logic-Based Program Synthesis and Transformation | 2011-05-27 | Paper |
Map fusion for nested datatypes in intensional type theory
Science of Computer Programming | 2011-02-21 | Paper |
An induction principle for nested datatypes in intensional type theory
Journal of Functional Programming | 2009-10-28 | Paper |
Monadic Translation of Intuitionistic Sequent Calculus
Lecture Notes in Computer Science | 2009-07-02 | Paper |
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
Logical Methods in Computer Science | 2009-06-30 | Paper |
A Datastructure for Iterated Powers
Lecture Notes in Computer Science | 2009-04-02 | Paper |
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
Lecture Notes in Computer Science | 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
Lecture Notes in Computer Science | 2008-08-28 | Paper |
Recursion on Nested Datatypes in Dependent Type Theory
Logic and Theory of Algorithms | 2008-06-19 | Paper |
Verification of the Redecoration Algorithm for Triangular Matrices
Lecture Notes in Computer Science | 2008-06-03 | Paper |
| Stabilization -- an alternative to double-negation translation for classical natural deduction | 2006-07-03 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2005-08-22 | Paper |
Non-strictly positive fixed points for classical natural deduction
Annals of Pure and Applied Logic | 2005-04-21 | Paper |
Iteration and coiteration schemes for higher-order and nested datatypes
Theoretical Computer Science | 2005-04-06 | Paper |
Substitution in non-wellfounded syntax with variable binding
Theoretical Computer Science | 2005-01-11 | Paper |
| scientific article; zbMATH DE number 2006636 (Why is no real title available?) | 2003-11-23 | Paper |
| scientific article; zbMATH DE number 2003147 (Why is no real title available?) | 2003-11-12 | Paper |
Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
Archive for Mathematical Logic | 2003-09-16 | Paper |
| scientific article; zbMATH DE number 1956505 (Why is no real title available?) | 2003-07-30 | Paper |
Tarski's fixed-point theorem and lambda calculi with monotone inductive types
Synthese | 2003-04-27 | Paper |
| scientific article; zbMATH DE number 1841846 (Why is no real title available?) | 2002-12-04 | Paper |
| A locally trivial quantum Hopf bundle | 2002-10-14 | Paper |
| scientific article; zbMATH DE number 1722662 (Why is no real title available?) | 2002-03-21 | Paper |
| scientific article; zbMATH DE number 1615235 (Why is no real title available?) | 2001-07-08 | Paper |
Monotone (co)inductive types and positive fixed-point types
RAIRO - Theoretical Informatics and Applications | 2000-07-24 | Paper |
Monotone (co)inductive types and positive fixed-point types
RAIRO - Theoretical Informatics and Applications | 2000-07-24 | Paper |
| scientific article; zbMATH DE number 1342219 (Why is no real title available?) | 2000-03-29 | Paper |
| scientific article; zbMATH DE number 1385477 (Why is no real title available?) | 2000-01-09 | Paper |
