| Publication | Date of Publication | Type |
|---|
| A type theory for defining logics and proofs | 2024-12-19 | Paper |
| Normalization by evaluation for modal dependent type theory | 2023-12-11 | Paper |
| A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types | 2022-12-08 | Paper |
| Harpoon: mechanizing metatheory interactively | 2021-12-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4993349 | 2021-06-15 | Paper |
| Contextual Types, Explained | 2021-01-21 | Paper |
| Semantical analysis of contextual types | 2020-09-23 | Paper |
| POPLMark reloaded: Mechanizing proofs by logical relations | 2020-05-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5111317 | 2020-05-26 | Paper |
| A case study in programming coinductive proofs: Howe’s method | 2019-10-09 | Paper |
| Programming type-safe transformations using higher-order abstract syntax | 2019-09-18 | Paper |
| Mechanizing proofs with logical relations – Kripke-style | 2018-10-19 | Paper |
| Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions | 2018-10-19 | Paper |
| Well-founded recursion with copatterns and sized types | 2017-10-23 | Paper |
| Contextual modal type theory | 2017-07-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5277845 | 2017-07-12 | Paper |
| Programs Using Syntax with First-Class Binders | 2017-05-19 | Paper |
| LINCX: A Linear Logical Framework with First-Class Contexts | 2017-05-19 | Paper |
| Indexed codata types | 2017-05-10 | Paper |
| The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey | 2016-05-26 | Paper |
| Case analysis of higher-order data | 2016-05-06 | Paper |
| Inductive Beluga: Programming Proofs | 2015-12-02 | Paper |
| Higher-order term indexing using substitution trees | 2015-09-17 | Paper |
| Programming with binders and indexed data-types | 2015-09-11 | Paper |
| Wellfounded recursion with copatterns | 2015-03-30 | Paper |
| Programming Type-Safe Transformations Using Higher-Order Abstract Syntax | 2015-01-13 | Paper |
| Copatterns | 2014-11-27 | Paper |
| A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions | 2014-09-12 | Paper |
| Unnesting of Copatterns | 2014-07-24 | Paper |
| Fair reactive programming | 2014-04-10 | Paper |
| Focusing the inverse method for LF: a preliminary report | 2014-01-10 | Paper |
| Functional programming with higher-order abstract syntax and explicit substitutions | 2013-12-13 | Paper |
| An insider's look at LF type reconstruction: everything you (n)ever wanted to know | 2013-03-28 | Paper |
| Higher-Order Dynamic Pattern Unification for Dependent Types and Records | 2011-06-17 | Paper |
| Programming Inductive Proofs | 2010-11-22 | Paper |
| Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description) | 2010-09-14 | Paper |
| Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison | 2010-09-14 | Paper |
| Automated Deduction – CADE-19 | 2010-04-20 | Paper |
| Logic Programming | 2009-08-06 | Paper |
| Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach | 2009-03-12 | Paper |
| Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4 | 2009-03-06 | Paper |
| Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF | 2008-09-02 | Paper |
| Overcoming Performance Barriers: Efficient Verification Techniques for Logical Frameworks | 2008-03-11 | Paper |
| Verifying termination and reduction properties about higher-order logic programs | 2006-11-03 | Paper |
| Automated Deduction – CADE-20 | 2006-11-01 | Paper |
| Logic Programming | 2006-06-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4812964 | 2004-08-12 | Paper |
| Connection-driven inductive theorem proving | 2002-09-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4539625 | 2002-07-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4530465 | 2002-06-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2721203 | 2001-07-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4934147 | 2000-01-17 | Paper |
