| Publication | Date of Publication | Type |
|---|
| The Münchhausen method in type theory | 2024-11-26 | Paper |
| Combinatory logic and lambda calculus are equal, algebraically | 2024-10-21 | Paper |
| Proving strong normalization of CC by modifying realizability semantics | 2023-12-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q6079230 | 2023-10-27 | Paper |
| Naïve Type Theory | 2023-09-20 | Paper |
| Categorical reconstruction of a reduction free normalization proof | 2022-12-16 | Paper |
| Martin Hofmann’s contributions to type theory: Groupoids and univalence | 2022-06-24 | Paper |
| Should Type Theory replace Set Theory as the Foundation of Mathematics | 2021-11-11 | Paper |
| Constructing a universe for the setoid model | 2021-10-18 | Paper |
| The Integers as a Higher Inductive Type | 2021-01-21 | Paper |
| Free Higher Groups in Homotopy Type Theory | 2021-01-20 | Paper |
| Setoid type theory -- a syntactic translation | 2020-05-05 | Paper |
| Relative Monads Formalised | 2019-09-18 | Paper |
| Towards a Cubical Type Theory without an Interval | 2018-08-13 | Paper |
| Quotient inductive-inductive types | 2018-07-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5371043 | 2017-10-24 | Paper |
| Indexed containers | 2017-10-23 | Paper |
| Normalisation by Evaluation for Dependent Types. | 2017-10-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5278407 | 2017-07-19 | Paper |
| Partiality, Revisited | 2017-05-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2980980 | 2017-05-08 | Paper |
| Type theory in type theory using quotient inductive types | 2016-10-24 | Paper |
| Monads need not be endofunctors | 2015-03-11 | Paper |
| A Partial Type Checking Algorithm for Type:Type | 2014-06-27 | Paper |
| From reversible to irreversible computations | 2014-01-17 | Paper |
| An algebra of pure quantum programming | 2013-12-06 | Paper |
| Generalizations of Hedberg’s Theorem | 2013-06-28 | Paper |
| Small Induction Recursion | 2013-06-28 | Paper |
| When is a function a fold or an unfold? | 2013-04-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4649535 | 2012-11-22 | Paper |
| A Categorical Semantics for Inductive-Inductive Definitions | 2011-09-02 | Paper |
| Higher-order containers | 2010-07-29 | Paper |
| Subtyping, Declaratively | 2010-07-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3560840 | 2010-05-14 | Paper |
| ΠΣ: Dependent Types without the Sugar | 2010-05-04 | Paper |
| Monads Need Not Be Endofunctors | 2010-04-27 | Paper |
| Big-step normalisation | 2009-10-28 | Paper |
| A UNIVERSE OF STRICTLY POSITIVE FAMILIES | 2009-04-14 | Paper |
| Functional and Logic Programming | 2007-09-25 | Paper |
| Types for Proofs and Programs | 2006-11-13 | Paper |
| Structuring quantum effects: superoperators as arrows | 2006-08-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4816996 | 2004-09-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2766796 | 2002-07-22 | Paper |
| A predicative analysis of structural recursion | 2002-04-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2778814 | 2002-03-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2778813 | 2002-03-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4945244 | 2000-09-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4263807 | 2000-04-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4281462 | 1994-03-10 | Paper |
