Research
My research spans both pure mathematics and computer science.
In mathematics, I work on the theory and applications of low- and higher-dimensional generalised categorical structures, often developed through two- and three-dimensional universal algebra. This programme connects naturally with areas such as proof theory, the geometry of manifolds, algebraic topology, universal algebra, logic, and related fields.
In computer science, I work in programming language semantics, formal methods, and software technology, with particular emphasis on correctness-by-construction approaches to the design and implementation of programming languages. My research combines rigorous semantic analysis with questions arising from the engineering of modern programming paradigms.
More broadly, I am committed to the systematic use of formal and mathematical structures in computer science and software engineering. I regard structural and logical methods not as external tools, but as foundations for sound design. The aim is to develop coherent theories that guide implementation and yield systems that are reliable, transparent, and conceptually well-founded.
I welcome discussions and collaborations with researchers and prospective Ph.D. students working in categorical structures, programming language theory, formal methods, software technology, or closely related areas. Please feel free to get in touch.
Selected publications
- Monoidal closure of Grothendieck constructions via Σ-tractable monoidal structures and Dialectica formulas Theory and Applications of Categories, 44, 1153–1217, 2025. (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, 180–226, 2024. (arXiv)
- Lax comma categories: cartesian closedness, extensivity, topologicity, and descent Theory and Applications of Categories, 41, 516–530, 2024. (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. (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), 2022. (DOI; arXiv)
- Descent data and absolute Kan extensions Theory and Applications of Categories, 37, 530–561, 2021. (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. (arXiv)
- Pseudo-Kan extensions and descent theory Theory and Applications of Categories, 33, 390–444, 2018. (arXiv)
- On biadjoint triangles Theory and Applications of Categories, 31, 217–256, 2016. (arXiv)
Accepted for publication
- Unraveling the iterative CHAD Accepted for publication in Mathematical Structures in Computer Science.
- Free doubly-infinitary distributive categories are cartesian closed Accepted for publication in Applied Categorical Structures.
Preprints under review
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.
- Freely generated categorical structures and automatic differentiation Computer Science Ph.D. thesis, Utrecht University, 2025.
- Pseudomonads and descent Mathematics Ph.D. thesis, University of Coimbra, 2017.
- 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
For information about current and former Ph.D. students, please see the Ph.D. supervision page. For a full and regularly updated list of publications, invited talks, teaching, supervision, service, and academic appointments, please see my Curriculum Vitae.