| May 2025 | Internal Effectful Forcing in System T |
| with Martín H. Escardó, Bruno da Rocha Paiva, Vincent Rahli | |
| arXiv, formalization | |
| Aug. 2023 | Inductive Continuity via Brouwer Trees |
| with Liron Cohen, Vincent Rahli, Bruno da Rocha Paiva | |
| DOI | |
| Jul. 2022 | Patch Locale of a Spectral Locale in Univalent Type Theory |
| with Martín H. Escardó | |
| DOI, arXiv | |
| Aug. 2021 | Formal Topology and Univalent Foundations |
| with Thierry Coquand |
| Feb 2024 | The Patch Topology in Univalent Foundations |
| with Igor Arrieta, Martín H. Escardó | |
| arXiv |
| Jun. 2025 | Predicative Stone Duality in Univalent Foundations |
| at TYPES 2025 | |
| slides, abstract | |
| Mar. 2024 | Locale Theory in Univalent Foundations |
| at ASSUME | |
| slides | |
| Aug. 2023 | Inductive Continuity via Brouwer Trees |
| at MFCS 2023 | |
| slides | |
| Mar. 2023 | The Patch Locale of a Spectral Locale in Univalent Type Theory |
| at YaMCATS 30 | |
| slides | |
| Jun. 2022 | The Patch Locale of a Spectral Locale in Univalent Type Theory |
| at TYPES 2022 | |
| slides, abstract | |
| Feb. 2020 | Formal Topology in Univalent Foundations |
| at Goteborg-Stockholm Type Theory Seminar | |
| slides, abstract |
| June 2025 | Constructive and Predicative Locale Theory in Univalent Foundations |
| PhD thesis at University of Birmingham | |
| Defended on February 27, 2025 | |
| Examiners: Eric Finster, Bas Spitters | |
| May 2020 | Formal Topology in Univalent Foundations |
| MSc thesis at Chalmers University of Technology | |
| Examiner: Nils Anders Danielsson | |
| pdf, slides |