| Publication | Date of Publication | Type |
|---|
| Semantics for two-dimensional type theory | 2024-12-06 | Paper |
| Univalent monoidal categories | 2024-11-26 | Paper |
Bicategorical type theory: semantics and syntax
Mathematical Structures in Computer Science | 2024-03-05 | Paper |
| Univalent Double Categories | 2023-10-13 | Paper |
Univalent Foundations and the Equivalence Principle
Synthese Library | 2023-09-20 | Paper |
| Formalizing Monoidal Categories and Actions for Syntax with Binders | 2023-07-30 | Paper |
Bicategories in univalent foundations
Mathematical Structures in Computer Science | 2022-12-09 | Paper |
| Univalent Monoidal Categories | 2022-12-06 | Paper |
| Category Theory for Programming | 2022-09-02 | Paper |
scientific article; zbMATH DE number 7559272 (Why is no real title available?)
(available as arXiv preprint) | 2022-07-18 | Paper |
scientific article; zbMATH DE number 7559271 (Why is no real title available?)
(available as arXiv preprint) | 2022-07-18 | Paper |
| High-level signatures and initial semantics | 2022-05-28 | Paper |
| Implementing a Category-Theoretic Framework for Typed Abstract Syntax | 2021-12-13 | Paper |
| Algebraic Presentations of Dependent Type Theories | 2021-11-18 | Paper |
scientific article; zbMATH DE number 7379288 (Why is no real title available?)
(available as arXiv preprint) | 2021-08-05 | Paper |
| The Univalence Principle | 2021-02-11 | Paper |
A higher structure identity principle
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-21 | Paper |
| Displayed Categories | 2020-05-26 | Paper |
| scientific article; zbMATH DE number 7204300 (Why is no real title available?) | 2020-05-26 | Paper |
Initial semantics for higher-order typed syntax in \textsf{Coq}
(available as arXiv preprint) | 2019-09-18 | Paper |
Initiality for typed syntax and semantics
(available as arXiv preprint) | 2019-09-18 | Paper |
From signatures to monads in \textsf{UniMath}
Journal of Automated Reasoning | 2019-08-21 | Paper |
Initial semantics for reduction rules
(available as arXiv preprint) | 2019-05-17 | Paper |
Displayed categories
(available as arXiv preprint) | 2019-03-18 | Paper |
Bicategories in Univalent Foundations
(available as arXiv preprint) | 2019-03-04 | Paper |
Modular specification of monads through higher-order presentations
(available as arXiv preprint) | 2019-03-03 | Paper |
Categorical structures for type theory in univalent foundations
(available as arXiv preprint) | 2018-09-26 | Paper |
Heterogeneous substitution systems revisited
(available as arXiv preprint) | 2018-08-13 | Paper |
Non-wellfounded trees in homotopy type theory
(available as arXiv preprint) | 2017-07-12 | Paper |
Terminal semantics for codata types in intensional Martin-Löf type theory
(available as arXiv preprint) | 2017-07-12 | Paper |
Some Wellfounded Trees in UniMath
Mathematical Software – ICMS 2016 | 2016-09-28 | Paper |
Modules over relative monads for syntax and semantics
Mathematical Structures in Computer Science | 2016-07-28 | Paper |
Univalent categories and the Rezk completion
Mathematical Structures in Computer Science | 2016-07-27 | Paper |
Initiality for typed syntax and semantics
Logic, Language, Information and Computation | 2012-09-21 | Paper |
Extended initiality for typed abstract syntax
Logical Methods in Computer Science | 2012-05-16 | Paper |
Insights From Univalent Foundations: A Case Study Using Double Categories
(available as arXiv preprint) | N/A | Paper |
