| 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
Journal Of Logic And Computation | 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
Mathematical Structures in Computer Science | 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
Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics | 2021-12-08 | Paper |
A Note on Generalized Algebraic Theories and Categories with Families
(available as arXiv preprint) | 2020-12-15 | Paper |
Internal type theory
Lecture Notes in Computer Science | 2019-01-15 | Paper |
Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids
Lecture Notes in Computer Science | 2019-01-15 | Paper |
scientific article; zbMATH DE number 6816943 (Why is no real title available?)
(available as arXiv preprint) | 2017-12-11 | Paper |
| Undecidability of equality in the free locally Cartesian closed category | 2017-07-12 | Paper |
The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
Mathematical Structures in Computer Science | 2016-07-26 | Paper |
Game semantics and normalization by evaluation
Lecture Notes in Computer Science | 2015-10-01 | Paper |
Normalization by Evaluation for Martin-Löf Type Theory with One Universe
Electronic Notes in Theoretical Computer Science | 2015-07-10 | Paper |
Program testing and the meaning explanations of intuitionistic type theory
Epistemology versus Ontology | 2015-06-05 | Paper |
The interpretation of intuitionistic type theory in locally Cartesian closed categories -- an intuitionistic perspective
Electronic Notes in Theoretical Computer Science | 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
Foundations of Software Science and Computational Structures | 2012-06-22 | Paper |
Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation
Annals of Pure and Applied Logic | 2011-12-12 | Paper |
The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
Lecture Notes in Computer Science | 2011-06-17 | Paper |
A Brief Overview of Agda – A Functional Language with Dependent Types
Lecture Notes in Computer Science | 2009-10-20 | Paper |
Dependent Types at Work
Language Engineering and Rigorous Software Development | 2009-07-28 | Paper |
Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
Lecture Notes in Computer Science | 2008-08-28 | Paper |
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
Functional and Logic Programming | 2008-04-11 | Paper |
Indexed induction-recursion
The Journal of Logic and Algebraic Programming | 2005-12-22 | Paper |
Theoretical Aspects of Computing - ICTAC 2004
Lecture Notes in Computer Science | 2005-11-30 | Paper |
| scientific article; zbMATH DE number 2111733 (Why is no real title available?) | 2004-10-28 | Paper |
| scientific article; zbMATH DE number 2090724 (Why is no real title available?) | 2004-08-13 | Paper |
| scientific article; zbMATH DE number 2077110 (Why is no real title available?) | 2004-07-01 | Paper |
Induction-recursion and initial algebras.
Annals of Pure and Applied Logic | 2003-11-25 | Paper |
| scientific article; zbMATH DE number 2006633 (Why is no real title available?) | 2003-11-23 | Paper |
A general formulation of simultaneous inductive-recursive definitions in type theory
Journal of Symbolic Logic | 2000-10-03 | Paper |
| scientific article; zbMATH DE number 1342277 (Why is no real title available?) | 1999-09-22 | Paper |
Normalization and the Yoneda embedding
Mathematical Structures in Computer Science | 1999-08-17 | Paper |
Representing inductively defined sets by wellorderings in Martin-Löf's type theory
Theoretical Computer Science | 1998-07-27 | Paper |
Intuitionistic model constructions and normalization proofs
MSCS. Mathematical Structures in Computer Science | 1998-03-23 | Paper |
Inductive families
Formal Aspects of Computing | 1994-10-26 | Paper |
| scientific article; zbMATH DE number 65535 (Why is no real title available?) | 1992-09-27 | Paper |
Inverse image analysis generalises strictness analysis
Information and Computation | 1991-01-01 | Paper |
Comparing integrated and external logics of functional programs
Science of Computer Programming | 1990-01-01 | Paper |
A functional programming approach to the specification and verification of concurrent systems
Formal Aspects of Computing | 1989-01-01 | Paper |
| scientific article; zbMATH DE number 4011905 (Why is no real title available?) | 1987-01-01 | Paper |
| scientific article; zbMATH DE number 4007695 (Why is no real title available?) | 1986-01-01 | Paper |
| scientific article; zbMATH DE number 3907752 (Why is no real title available?) | 1985-01-01 | Paper |
| scientific article; zbMATH DE number 3898208 (Why is no real title available?) | 1985-01-01 | Paper |
| scientific article; zbMATH DE number 3881863 (Why is no real title available?) | 1984-01-01 | Paper |
Some results on the deductive structure of join dependencies
Theoretical Computer Science | 1984-01-01 | Paper |
| scientific article; zbMATH DE number 3876647 (Why is no real title available?) | 1982-01-01 | Paper |
