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.
Download here
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.
Recommended citation: https://doi.org/10.1145/3636501.3636956
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.
Recommended citation: https://doi.org/10.4230/LIPIcs.TYPES.2022.15