| Publication | Date of Publication | Type |
|---|
| Cubical Agda: A dependently typed programming language with univalence and higher inductive types | 2021-12-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4995161 | 2021-06-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5854733 | 2021-03-17 | Paper |
| Leibniz equality is isomorphic to Martin-Löf identity, parametrically | 2020-09-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3300787 | 2020-07-30 | Paper |
| POPLMark reloaded: Mechanizing proofs by logical relations | 2020-05-26 | Paper |
| Elaborating dependent (co)pattern matching: No pattern left behind | 2020-05-26 | Paper |
| Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality | 2019-11-19 | Paper |
| Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus | 2019-02-16 | Paper |
| Well-founded recursion with copatterns and sized types | 2017-10-23 | Paper |
| Interactive programming in Agda – Objects and graphical user interfaces | 2017-10-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5277845 | 2017-07-12 | Paper |
| Compositional Coinduction with Sized Types | 2016-07-15 | Paper |
| A Formalized Proof of Strong Normalization for Guarded Recursive Types | 2016-02-26 | Paper |
| Normalization by Evaluation for Martin-Löf Type Theory with One Universe | 2015-07-10 | Paper |
| Wellfounded recursion with copatterns | 2015-03-30 | Paper |
| Copatterns | 2014-11-27 | Paper |
| Unnesting of Copatterns | 2014-07-24 | Paper |
| A Partial Type Checking Algorithm for Type:Type | 2014-06-27 | Paper |
| Normalization for the Simply-Typed Lambda-Calculus in Twelf | 2014-01-10 | Paper |
| A Third-Order Representation of the λμ-Calculus | 2013-07-24 | Paper |
| On Irrelevance and Algorithmic Equality in Predicative Type Theory | 2012-04-03 | Paper |
| Higher-Order Dynamic Pattern Unification for Dependent Types and Records | 2011-06-17 | Paper |
| A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance | 2011-05-26 | Paper |
| Irrelevance in Type Theory with a Heterogeneous Equality Judgement | 2011-05-19 | Paper |
| Towards Normalization by Evaluation for the βη-Calculus of Constructions | 2010-05-04 | Paper |
| Typed Applicative Structures and Normalization by Evaluation for System F ω | 2009-11-12 | Paper |
| Implementing a normalizer using sized heterogeneous types | 2009-10-28 | Paper |
| Type-based termination of generic programs | 2009-07-24 | Paper |
| A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance | 2009-07-07 | Paper |
| Towards Generic Programming with Sized Types | 2009-04-02 | Paper |
| Semi-continuous Sized Types and Termination | 2009-03-12 | Paper |
| Strong Normalization and Equi-(Co)Inductive Types | 2009-03-10 | Paper |
| Weak βη-Normalization and Normalization by Evaluation for System F | 2009-01-27 | Paper |
| Syntactic Metatheory of Higher-Order Subtyping | 2008-11-20 | Paper |
| Polarised subtyping for sized types | 2008-11-13 | Paper |
| Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory | 2008-08-28 | Paper |
| Semi-continuous Sized Types and Termination | 2008-08-07 | Paper |
| Mixed Inductive/Coinductive Types and Strong Normalization | 2008-05-15 | Paper |
| On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory | 2008-04-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3593498 | 2007-07-20 | Paper |
| Polarized Subtyping for Sized Types | 2007-05-02 | Paper |
| Frontiers of Combining Systems | 2006-10-10 | Paper |
| Typed Lambda Calculi and Applications | 2005-11-11 | Paper |
| Computer Science Logic | 2005-08-22 | Paper |
| Iteration and coiteration schemes for higher-order and nested datatypes | 2005-04-06 | Paper |
| Termination checking with types | 2005-03-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4457444 | 2004-03-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4435457 | 2003-11-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4417851 | 2003-07-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2766795 | 2002-07-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2766796 | 2002-07-22 | Paper |
| A predicative analysis of structural recursion | 2002-04-17 | Paper |
