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
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.
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.
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.