2024
Internal Parametricity, without an Interval.
Proc. ACM Program. Lang., January, 2024
Synthetic 1-Categories in Directed Type Theory.
CoRR, 2024
Formalising inductive and coinductive containers.
CoRR, 2024
2023
Combinatory Logic and Lambda Calculus Are Equal, Algebraically.
Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction, 2023
2022
The Münchhausen Method in Type Theory.
Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022
2021
Martin Hofmann's contributions to type theory: Groupoids and univalence.
Math. Struct. Comput. Sci., 2021
Should Type Theory replace Set Theory as the Foundation of Mathematics.
CoRR, 2021
Constructing a universe for the setoid model.
Proceedings of the Foundations of Software Science and Computation Structures, 2021
2020
The Integers as a Higher Inductive Type.
Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020
2019
Constructing quotient inductive-inductive types.
Proc. ACM Program. Lang., 2019
Fundam. Informaticae, 2019
Big Step Normalisation for Type Theory.
Proceedings of the 25th International Conference on Types for Proofs and Programs, 2019
Setoid Type Theory - A Syntactic Translation.
Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019
2018
Free Higher Groups in Homotopy Type Theory.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018
Pure Functional Epidemics: An Agent-Based Approach.
Proceedings of the 30th Symposium on Implementation and Application of Functional Languages, 2018
Quotient Inductive-Inductive Types.
Proceedings of the Foundations of Software Science and Computation Structures, 2018
2017
Normalisation by Evaluation for Type Theory, in Type Theory.
Log. Methods Comput. Sci., 2017
Notions of Anonymous Existence in Martin-Löf Type Theory.
Log. Methods Comput. Sci., 2017
Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type.
Proceedings of the Foundations of Software Science and Computation Structures, 2017
2016
Selected papers from Dependently Typed Programming 2010 - Overview.
Math. Struct. Comput. Sci., 2016
Quotient inductive-inductive types.
CoRR, 2016
Normalisation by Evaluation for Dependent Types.
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016
Type theory in type theory using quotient inductive types.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016
Extending Homotopy Type Theory with Strict Equality.
Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016
2015
Monads need not be endofunctors.
Log. Methods Comput. Sci., 2015
Towards a Cubical Type Theory without an Interval.
Proceedings of the 21st International Conference on Types for Proofs and Programs, 2015
2014
Relative Monads Formalised.
J. Formaliz. Reason., 2014
Some constructions on ω-groupoids.
Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2014
2013
Generalizations of Hedberg's Theorem.
Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013
Small Induction Recursion.
Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013
2012
A Syntactical Approach to Weak omega-Groupoids.
Proceedings of the Computer Science Logic (CSL'12), 2012
2011
A Categorical Semantics for Inductive-Inductive Definitions.
Proceedings of the Algebra and Coalgebra in Computer Science, 2011
2010
Fundam. Informaticae, 2010
Subtyping, Declaratively.
Proceedings of the Mathematics of Program Construction, 10th International Conference, 2010
Termination Checking in the Presence of Nested Inductive and Coinductive Types.
Proceedings of the Partiality and Recursion in Interactive Theorem Provers, 2010
Hereditary Substitutions for Simple Types, Formalized.
Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, 2010
PiSigma: Dependent Types without the Sugar.
Proceedings of the Functional and Logic Programming, 10th International Symposium, 2010
Proceedings of the Programs, Proofs, Processes, 6th Conference on Computability in Europe, 2010
2009
A Universe of Strictly Positive Families.
Int. J. Found. Comput. Sci., 2009
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009
2008
A Partial Type Checking Algorithm for Type: Type.
Proceedings of the Second Workshop on Mathematically Structured Functional Programming, 2008
Dependent Types for Distributed Arrays.
Proceedings of the Nineth Symposium on Trends in Functional Programming, 2008
2007
Observational equality, now!
Proceedings of the ACM Workshop Programming Languages meets Program Verification, 2007
Proceedings of the ACM SIGPLAN Workshop on Haskell, 2007
Constructing Strictly Positive Families.
Proceedings of the Theory of Computing 2007. Proceedings of the Thirteenth Computing: The Australasian Theory Symposium (CATS2007). January 30, 2007
2006
Structuring quantum effects: superoperators as arrows.
Math. Struct. Comput. Sci., 2006
From Reversible to Irreversible Computations.
Proceedings of the 4th International Workshop on Quantum Programming Languages, 2006
Generic Programming with Dependent Types.
Proceedings of the Datatype-Generic Programming - International Spring School, 2006
Proceedings of the Workshop on Mathematically Structured Functional Programming, 2006
2005
Containers: Constructing strictly positive types.
Theor. Comput. Sci., 2005
for Data: Differentiating Data Structures.
Fundam. Informaticae, 2005
An Algebra of Pure Quantum Programming.
Proceedings of the 3rd International Workshop on Quantum Programming Languages, 2005
Epigram reloaded: a standalone typechecker for ETT.
Proceedings of the Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, 2005
A Functional Quantum Programming Language.
Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005
2004
Exploring the Regular Tree Types.
Proceedings of the Types for Proofs and Programs, International Workshop, 2004
Constructing Polymorphic Programs with Quotient Types.
Proceedings of the Mathematics of Program Construction, 7th International Conference, 2004
Representing Nested Inductive Types Using W-Types.
Proceedings of the Automata, Languages and Programming: 31st International Colloquium, 2004
Normalization by Evaluation for lambda<sup>-2</sup>.
Proceedings of the Functional and Logic Programming, 7th International Symposium, 2004
04381 Abstracts Collection - Dependently Typed Programming.
Proceedings of the Dependently Typed Programming, 12.09. - 17.09.2004, 2004
2003
Derivatives of Containers.
Proceedings of the Typed Lambda Calculi and Applications, 6th International Conference, 2003
Categories of Containers.
Proceedings of the Foundations of Software Science and Computational Structures, 2003
2002
A predicative analysis of structural recursion.
J. Funct. Program., 2002
Generic Programming within Dependently Typed Programming.
Proceedings of the Generic Programming, 2002
2001
When is a function a fold or an unfold?
Proceedings of the Coalgebraic Methods in Computer Science, 2001
A Finitary Subsystem of the Polymorphic lambda-Calculus.
Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001
Representations of First Order Function Types as Terminal Coalgebras.
Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001
Normalization by Evaluation for Typed Lambda Calculus with Coproducts.
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001
1999
A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types.
Proceedings of the Types for Proofs and Programs, 1999
Extensional Equality in Intensional Type Theory.
Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999
Monadic Presentations of Lambda Terms Using Generalized Inductive Types.
Proceedings of the Computer Science Logic, 13th International Workshop, 1999
1998
Logical Relations and Inductive/Coinductive Types.
Proceedings of the Computer Science Logic, 12th International Workshop, 1998
1996
Reduction-Free Normalisation for a Polymorphic System.
Proceedings of the Fourth Israel Symposium on Theory of Computing and Systems, 1996
1995
Categorical Reconstruction of a Reduction Free Normalization Proof.
Proceedings of the Category Theory and Computer Science, 6th International Conference, 1995
1993
Proving Strong Normalization of CC by Modifying Realizability Semantics.
Proceedings of the Types for Proofs and Programs, 1993
A Formalization of the Strong Normalization Proof for System F in LEGO.
Proceedings of the Typed Lambda Calculi and Applications, 1993
Constructions, inductive types and strong normalization.
PhD thesis, 1993