Portfolio item number 1
Short description of portfolio item number 1
Posts by Collection
portfolio
Portfolio item number 2
Short description of portfolio item number 2
publications
Univalent Monoidal Categories
Published in TYPES 2022 post-proceedings, 2023
This paper proves that the bicategory of monoidal categories is univalent and that monoidal categories admit Rezk completions.
Displayed Monoidal Categories for the Semantics of Linear Logic
Published in CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024
We present a formalization of different categorical structures used to interpret linear logic.
Substitution for Non-Wellfounded Syntax with Binders
Published in Proceedings of Formal Structures for Computation and Deduction (FSCD) 2024, 2024
We describe a generic construction of non-wellfounded syntax involving variable binding and its monadic substitution operation.
Scott’s Representation Theorem and the Univalent Karoubi Envelope
Published in ITP 2025: 16th International Conference on Interactive Theorem Proving, 2025
We present a formalization of Scott’s Representation Theorem in univalent foundations. Specifically, we implement two proofs of that theorem, one by Scott and one by Hyland. We also explain the role of the Karoubi envelope – a categorical construction – in the proofs and the impact the chosen foundation has on this construction
talks
Elementary topoi as categorical models of set theory
Published:
A seminar talk presented at The Antwerp Algebra Colloquium in the framework of the Master Program at the University of Antwerp.
Introduction to Type Theory: Another foundation of mathematics
Published:
A seminar talk presented at The Antwerp Algebra Colloquium
An introduction to Initial Algebra Semantics
Published:
A seminar talk presented at the Programming Languages Seminar.
Case Study on Displayed Monoidal Categories
Published:
A conference talk presented at TYPES 2022.
A Library of Monoidal Categories for Display and Univalence
Published:
A workshop talk presented (online) at the Workshop on Homotopy Type Theory/Univalent Foundations.
Rezk completions
Published:
A seminar talk at Dutch Categories And Types Seminar.
Rezk completion of bicategories
Published:
A workshop talk presented at the Workshop on Homotopy Type Theory/Univalent Foundations.
Formalizing Monoidal Categories and Actions for Syntax with Binders
Published:
A workshop talk presented (online) at the The Ninth International Workshop on Coq for Programming Languages.
Towards a homotopy theory of univalent category theory
Published:
A seminar talk presented (online) at USD Categories and Type Theory Seminar.
An introduction to proof assistants
Published:
A seminar talk presented at DIAM PhD Forum.
A formal treatment of univalent completions
Published:
A workshop talk presented at the Workshop on Homotopy Type Theory/Univalent Foundations.
A formal study of the Rezk completion
Published:
A workshop talk presented at the 30th International Conference on Types for Proofs and Programs.
Formal Theory of Rezk completions
Published:
A poster presentation given at the International Category Theory Conference. The poster can be found here.
Rezk completion for topoi
Published:
A seminar talk at Dutch Categories And Types Seminar.
From Realizability To Univalent Completions
Published:
A seminar talk presented at the Programming Languages Seminar.
Rezk Completions For (Elementary) Topoi
Published:
A workshop talk presented at the 31th International Conference on Types for Proofs and Programs.
teaching
Category Theory for Programmers
Mastercourse, Technical University of Delft, Programming Languages Group, 1900
Research project
Bachelor project supervision, Technical University of Delft, Programming Languages Group, 1900
Software verification
Mastercourse, Technical University of Delft, Programming Languages Group, 1900
Software verification
Mastercourse, Technical University of Delft, Programming Languages Group, 2022