Ph.D. in Computer Science
Freely Generated Categorical Structures and Automatic Differentiation
- Period November 2020 to November 2025
- Supervisors Professor Gabriele Keller and Dr. Matthijs Vákár.
- Committee Ieke Moerdijk, Bart Jacobs, Sam Staton, Robin Cockett, and Patricia Johann.
- Links Thesis material on arXiv
Main themes
Programming language semantics Categorical semantics Automatic differentiation CHAD Dual-numbers automatic differentiation Logical relations Program transformations Recursion and iteration Type systems Dependent types Algebraic effects Grothendieck constructions
Publications related to the Ph.D.
- CHAD for expressive total languages Mathematical Structures in Computer Science, 33(4–5), 311–426, 2023. 116 pages. (DOI; arXiv)
- Homomorphic reverse differentiation of iteration LAFI 2024, Tenth Workshop on Languages for Inference at POPL, 2024. 2 pages.
- Unraveling the iterative CHAD Accepted for publication in Mathematical Structures in Computer Science. arXiv:2505.15002, 2025, 58 pages.
- Logical relations for partial features and automatic differentiation correctness Oberwolfach Preprints, OWP-2023-09, 2023. arXiv:2210.08530, 2022, 25 pages.
- Automatic differentiation for ML-family languages: correctness via logical relations Mathematical Structures in Computer Science, 34(8), 747–806, 2024. 60 pages. (DOI; arXiv)
- Free doubly-infinitary distributive categories are cartesian closed Accepted for publication in Applied Categorical Structures. arXiv:2403.10447, 2024; revised 2026, 32 pages.
- Free extensivity via distributivity Portugaliae Mathematica, 82(1–2), 177–204, 2025. 28 pages. (DOI; arXiv)
- Monoidal closure of Grothendieck constructions via Σ-tractable monoidal structures and Dialectica formulas Theory and Applications of Categories, 44(35), 1153–1217, 2025. 65 journal pages. (Journal; arXiv)