| Publication | Date of Publication | Type |
|---|
| The Münchhausen method in type theory | 2024-11-26 | Paper |
| Combinatory logic and lambda calculus are equal, algebraically | 2024-10-21 | Paper |
Proving strong normalization of CC by modifying realizability semantics
Lecture Notes in Computer Science | 2023-12-08 | Paper |
| Big step normalisation for type theory | 2023-10-27 | Paper |
Naïve Type Theory
Synthese Library | 2023-09-20 | Paper |
Categorical reconstruction of a reduction free normalization proof
Category Theory and Computer Science | 2022-12-16 | Paper |
Martin Hofmann’s contributions to type theory: Groupoids and univalence
Mathematical Structures in Computer Science | 2022-06-24 | Paper |
| Should Type Theory replace Set Theory as the Foundation of Mathematics | 2021-11-11 | Paper |
| Constructing a universe for the setoid model | 2021-10-18 | Paper |
The integers as a higher inductive type
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-21 | Paper |
Free higher groups in homotopy type theory
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
Free higher groups in homotopy type theory
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
| Setoid type theory -- a syntactic translation | 2020-05-05 | Paper |
| Relative monads formalised | 2019-09-18 | Paper |
| Towards a cubical type theory without an interval | 2018-08-13 | Paper |
Quotient inductive-inductive types
(available as arXiv preprint) | 2018-07-17 | Paper |
Normalisation by evaluation for type theory, in type theory
(available as arXiv preprint) | 2017-10-24 | Paper |
Indexed containers
Journal of Functional Programming | 2017-10-23 | Paper |
| Normalisation by evaluation for dependent types | 2017-10-17 | Paper |
Extending homotopy type theory with strict equality
(available as arXiv preprint) | 2017-07-19 | Paper |
Partiality, Revisited
Lecture Notes in Computer Science | 2017-05-19 | Paper |
Notions of anonymous existence in Martin-Löf type theory
(available as arXiv preprint) | 2017-05-08 | Paper |
Type theory in type theory using quotient inductive types
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2016-10-24 | Paper |
Monads need not be endofunctors
Logical Methods in Computer Science | 2015-03-11 | Paper |
A partial type checking algorithm for Type:Type
Electronic Notes in Theoretical Computer Science | 2014-06-27 | Paper |
From reversible to irreversible computations
Electronic Notes in Theoretical Computer Science | 2014-01-17 | Paper |
An algebra of pure quantum programming
Electronic Notes in Theoretical Computer Science | 2013-12-06 | Paper |
Generalizations of Hedberg's theorem
Lecture Notes in Computer Science | 2013-06-28 | Paper |
Small induction recursion
Lecture Notes in Computer Science | 2013-06-28 | Paper |
When is a function a fold or an unfold?
Electronic Notes in Theoretical Computer Science | 2013-04-26 | Paper |
| A syntactical approach to weak omega-groupoids | 2012-11-22 | Paper |
A categorical semantics for inductive-inductive definitions
Algebra and Coalgebra in Computer Science | 2011-09-02 | Paper |
Higher-order containers
Programs, Proofs, Processes | 2010-07-29 | Paper |
Subtyping, declaratively. An exercise in mixed induction and coinduction
Lecture Notes in Computer Science | 2010-07-26 | Paper |
| The quantum IO monad | 2010-05-14 | Paper |
\(\Pi \Sigma \): dependent types without the sugar
Functional and Logic Programming | 2010-05-04 | Paper |
Monads need not be endofunctors
Foundations of Software Science and Computational Structures | 2010-04-27 | Paper |
Big-step normalisation
Journal of Functional Programming | 2009-10-28 | Paper |
A UNIVERSE OF STRICTLY POSITIVE FAMILIES
International Journal of Foundations of Computer Science | 2009-04-14 | Paper |
Functional and Logic Programming
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Types for Proofs and Programs
Lecture Notes in Computer Science | 2006-11-13 | Paper |
Structuring quantum effects: superoperators as arrows
Mathematical Structures in Computer Science | 2006-08-28 | Paper |
| scientific article; zbMATH DE number 2100542 (Why is no real title available?) | 2004-09-14 | Paper |
| scientific article; zbMATH DE number 1696607 (Why is no real title available?) | 2002-07-22 | Paper |
A predicative analysis of structural recursion
Journal of Functional Programming | 2002-04-17 | Paper |
| scientific article; zbMATH DE number 1722646 (Why is no real title available?) | 2002-03-21 | Paper |
| scientific article; zbMATH DE number 1722645 (Why is no real title available?) | 2002-03-21 | Paper |
| scientific article; zbMATH DE number 1424053 (Why is no real title available?) | 2000-09-20 | Paper |
| scientific article; zbMATH DE number 1342222 (Why is no real title available?) | 2000-04-25 | Paper |
| scientific article; zbMATH DE number 512769 (Why is no real title available?) | 1994-03-10 | Paper |
