| Publication | Date of Publication | Type |
|---|
| Type theory with explicit universe polymorphism | 2024-11-26 | Paper |
| The extended predicative Mahlo universe in Martin-Löf type theory | 2024-11-12 | Paper |
| A comparison of HOL and ALF formalizations of a categorical coherence theorem | 2024-07-05 | Paper |
| On generalized algebraic theories and categories with families | 2022-06-24 | Paper |
| Finitary higher inductive types in the groupoid model | 2022-04-25 | Paper |
| Categories with Families: Unityped, Simply Typed, and Dependently Typed | 2021-12-08 | Paper |
| A Note on Generalized Algebraic Theories and Categories with Families | 2020-12-15 | Paper |
| Internal type theory | 2019-01-15 | Paper |
| Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids | 2019-01-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4596801 | 2017-12-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5277836 | 2017-07-12 | Paper |
| The biequivalence of locally cartesian closed categories and Martin-Löf type theories | 2016-07-26 | Paper |
| Game Semantics and Normalization by Evaluation | 2015-10-01 | Paper |
| Normalization by Evaluation for Martin-Löf Type Theory with One Universe | 2015-07-10 | Paper |
| Program Testing and the Meaning Explanations of Intuitionistic Type Theory | 2015-06-05 | Paper |
| The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective | 2014-05-13 | Paper |
| Towards formalizing categorical models of type theory in type theory | 2014-01-10 | Paper |
| Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs | 2012-06-22 | Paper |
| Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation | 2011-12-12 | Paper |
| The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories | 2011-06-17 | Paper |
| A Brief Overview of Agda – A Functional Language with Dependent Types | 2009-10-20 | Paper |
| Dependent Types at Work | 2009-07-28 | Paper |
| Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory | 2008-08-28 | Paper |
| On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory | 2008-04-11 | Paper |
| Indexed induction-recursion | 2005-12-22 | Paper |
| Theoretical Aspects of Computing - ICTAC 2004 | 2005-11-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4825542 | 2004-10-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4813224 | 2004-08-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4470492 | 2004-07-01 | Paper |
| Induction-recursion and initial algebras. | 2003-11-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4436029 | 2003-11-23 | Paper |
| A general formulation of simultaneous inductive-recursive definitions in type theory | 2000-10-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4263867 | 1999-09-22 | Paper |
| Normalization and the Yoneda embedding | 1999-08-17 | Paper |
| Representing inductively defined sets by wellorderings in Martin-Löf's type theory | 1998-07-27 | Paper |
| Intuitionistic model constructions and normalization proofs | 1998-03-23 | Paper |
| Inductive families | 1994-10-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4012883 | 1992-09-27 | Paper |
| Inverse image analysis generalises strictness analysis | 1991-01-01 | Paper |
| Comparing integrated and external logics of functional programs | 1990-01-01 | Paper |
| A functional programming approach to the specification and verification of concurrent systems | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3761674 | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3757369 | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3685173 | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3677148 | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3216122 | 1984-01-01 | Paper |
| Some results on the deductive structure of join dependencies | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3341950 | 1982-01-01 | Paper |
