| Publication | Date of Publication | Type |
|---|
| A categorical normalization proof for the modal lambda-calculus | 2026-04-02 | Paper |
| A modal analysis of metaprogramming, revisited (invited talk) | 2026-02-24 | Paper |
| Adjoint natural deduction | 2026-01-14 | Paper |
| Multi-level contextual type theory | 2025-08-19 | Paper |
| A case study on logical relations using contextual types | 2025-08-19 | Paper |
| An open challenge problem repository for systems supporting binders | 2025-08-19 | Paper |
| Explicit substitutions for contextual type theory | 2025-08-19 | Paper |
| A type theory for defining logics and proofs | 2024-12-19 | Paper |
Normalization by evaluation for modal dependent type theory
Journal of Functional Programming | 2023-12-11 | Paper |
A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types
ACM Transactions on Computational Logic | 2022-12-08 | Paper |
| Harpoon: mechanizing metatheory interactively | 2021-12-01 | Paper |
Index-stratified types
(available as arXiv preprint) | 2021-06-15 | Paper |
Contextual types, explained. Invited tutorial
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-21 | Paper |
| Semantical analysis of contextual types | 2020-09-23 | Paper |
| scientific article; zbMATH DE number 7204440 (Why is no real title available?) | 2020-05-26 | Paper |
POPLMark reloaded: mechanizing proofs by logical relations
Journal of Functional Programming | 2020-05-26 | Paper |
A case study in programming coinductive proofs: Howe's method
Mathematical Structures in Computer Science | 2019-10-09 | Paper |
| Programming type-safe transformations using higher-order abstract syntax | 2019-09-18 | Paper |
Mechanizing proofs with logical relations -- Kripke-style
Mathematical Structures in Computer Science | 2018-10-19 | Paper |
Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
Mathematical Structures in Computer Science | 2018-10-19 | Paper |
Well-founded recursion with copatterns and sized types
Journal of Functional Programming | 2017-10-23 | Paper |
| Well-founded recursion over contextual objects | 2017-07-12 | Paper |
Contextual modal type theory
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Programs using syntax with first-class binders
Programming Languages and Systems | 2017-05-19 | Paper |
\textsc{Lincx}: a linear logical framework with first-class contexts
Programming Languages and Systems | 2017-05-19 | Paper |
Indexed codata types
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming | 2017-05-10 | Paper |
The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
Journal of Automated Reasoning | 2016-05-26 | Paper |
Case analysis of higher-order data
Electronic Notes in Theoretical Computer Science | 2016-05-06 | Paper |
Inductive beluga: programming proofs
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Higher-order term indexing using substitution trees
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Programming with binders and indexed data-types
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
Wellfounded recursion with copatterns: a unified approach to termination and productivity
Proceedings of the 18th ACM SIGPLAN international conference on Functional programming | 2015-03-30 | Paper |
Programming type-safe transformations using higher-order abstract syntax
Certified Programs and Proofs | 2015-01-13 | Paper |
Copatterns, programming infinite structures by observations
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-11-27 | Paper |
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-09-12 | Paper |
Unnesting of copatterns
Lecture Notes in Computer Science | 2014-07-24 | Paper |
Fair reactive programming
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 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
Electronic Notes in Theoretical Computer Science | 2013-12-13 | Paper |
An insider's look at LF type reconstruction: everything you (n)ever wanted to know
Journal of Functional Programming | 2013-03-28 | Paper |
Higher-order dynamic pattern unification for dependent types and records
Lecture Notes in Computer Science | 2011-06-17 | Paper |
Programming inductive proofs. A new approach based on contextual types
Verification, Induction, Termination Analysis | 2010-11-22 | Paper |
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
Automated Reasoning | 2010-09-14 | Paper |
Reasoning with higher-order abstract syntax and contexts: a comparison
Interactive Theorem Proving | 2010-09-14 | Paper |
Optimizing higher-order pattern unification.
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Logic Programming
Lecture Notes in Computer Science | 2009-08-06 | Paper |
Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach
Automated Reasoning | 2009-03-12 | Paper |
Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
Lecture Notes in Computer Science | 2008-09-02 | Paper |
Overcoming Performance Barriers: Efficient Verification Techniques for Logical Frameworks
Logic Programming | 2008-03-11 | Paper |
Verifying termination and reduction properties about higher-order logic programs
Journal of Automated Reasoning | 2006-11-03 | Paper |
Automated Deduction – CADE-20
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Logic Programming
Lecture Notes in Computer Science | 2006-06-27 | Paper |
| scientific article; zbMATH DE number 2090533 (Why is no real title available?) | 2004-08-12 | Paper |
Connection-driven inductive theorem proving
Studia Logica | 2002-09-16 | Paper |
| scientific article; zbMATH DE number 1765685 (Why is no real title available?) | 2002-07-10 | Paper |
| scientific article; zbMATH DE number 1748580 (Why is no real title available?) | 2002-06-03 | Paper |
| scientific article; zbMATH DE number 1612558 (Why is no real title available?) | 2001-07-01 | Paper |
| scientific article; zbMATH DE number 1389654 (Why is no real title available?) | 2000-01-17 | Paper |
