Research Programme
In computer science, I develop foundations that lead directly to practical solutions. My recent work centres on programming language semantics, formal methods, and software technology. In particular, I derive program transformations from semantic structure so that they are correct by construction and suitable for direct implementation.
In pure mathematics, my primary interests lie in the theory and applications of low- and higher-dimensional generalised categorical structures. I develop their foundations through two- and three-dimensional universal algebra, studying both their intrinsic structure and their connections with algebraic topology, geometry, logic, proof theory, and universal algebra, as well as their applications in computer science.
These directions form a single research programme in which problems from computer science and software engineering shape the mathematics from the outset. The resulting theory is developed both as mathematics in its own right and as a foundation for semantic models, correctness principles, and reliable methods for designing and implementing programming languages, program transformations, and software systems.
Browse by publication venue
Filter the record by the venue in which a work appeared or has been formally accepted. Submitted manuscripts remain under preprints until they have an accepted publication venue.
Selected preprints
Current work selected to represent the principal active strands of the research programme.
- From Grothendieck cofibrations to factorization systems: a formal 2-monadic account
- Simply typed reverse-mode automatic differentiation with variants: denotational correctness via idempotent completion
- Backpropagation for effectful languages I: finite probability and discrete output algebraic effects Submitted to POPL 2027.
- Unraveling the iterative CHAD Manuscript under revision.
- Functors preserving effective descent morphisms
- Freely generated n-categories, coinserters and presentations of low dimensional categories
Refereed journal publications
- Free doubly-infinitary distributive categories are cartesian closed Applied Categorical Structures, 34(5), article 53, 2026. (DOI; arXiv)
- Monoidal closure of Grothendieck constructions via Σ-tractable monoidal structures and Dialectica formulas Theory and Applications of Categories, 44(35), 1153–1217, 2025. (Journal; arXiv)
- Free extensivity via distributivity Portugaliae Mathematica, 82(1–2), 177–204, 2025. (DOI; arXiv)
- Generalized multicategories: change-of-base, embedding, and descent Applied Categorical Structures, 32, article 35, 2024. (DOI; arXiv)
- Lax comma 2-categories and admissible 2-functors Theory and Applications of Categories, 40(6), 180–226, 2024. (DOI; arXiv)
- Lax comma categories: cartesian closedness, extensivity, topologicity, and descent Theory and Applications of Categories, 41(16), 516–530, 2024. (DOI; arXiv)
- Automatic differentiation for ML-family languages: correctness via logical relations Mathematical Structures in Computer Science, 34(8), 747–806, 2024. (DOI; arXiv)
- Descent for internal multicategory functors Applied Categorical Structures, 31, article 11, 2023. (DOI; arXiv)
- Lax comma categories of ordered sets Quaestiones Mathematicae, 46, supplement 1, 145–159, 2023. (DOI; arXiv)
- CHAD for expressive total languages Mathematical Structures in Computer Science, 33(4–5), 311–426, 2023. (DOI; arXiv)
- Cauchy completeness, lax epimorphisms and effective descent for split fibrations Bulletin of the Belgian Mathematical Society Simon Stevin, 30(1), 130–139, 2023. (DOI; arXiv)
- Semantic factorization and descent Applied Categorical Structures, 30(6), 1393–1433, 2022. (DOI; arXiv)
- On lax epimorphisms and the associated factorization Journal of Pure and Applied Algebra, 226(12), article 107126, 2022. (DOI; arXiv)
- Descent data and absolute Kan extensions Theory and Applications of Categories, 37(18), 530–561, 2021. (DOI; arXiv)
- Pseudoalgebras and non-canonical isomorphisms Applied Categorical Structures, 27(1), 55–63, 2019. (DOI; arXiv)
- On lifting of biadjoints and lax algebras Categories and General Algebraic Structures with Applications, 9(1), 29–58, 2018. (DOI; arXiv)
- Pseudo-Kan extensions and descent theory Theory and Applications of Categories, 33(15), 390–444, 2018. (DOI; arXiv)
- On biadjoint triangles Theory and Applications of Categories, 31(9), 217–256, 2016. (DOI; arXiv)
Other publications
- Homomorphic reverse differentiation of iteration LAFI 2024, Tenth Workshop on Languages for Inference at POPL, 2024.
- Logical relations for partial features and automatic differentiation correctness Oberwolfach Preprints, OWP-2023-09, 2023. (DOI)
- Freely generated categorical structures and automatic differentiation Computer Science Ph.D. thesis, Utrecht University; approved, with the degree to be awarded in 2026.
- Pseudomonads and descent Mathematics Ph.D. thesis, 2017; degree awarded 2018.
- Espaços não reversíveis Revista Matemática Universitária, 48–49, 22–26, 2012.
Undergraduate and graduate monographs
- Basic concepts of topology for topological dynamics
- Basic topological dynamics and basic applications to number theory