I am a PhD candidate at the University of Amsterdam, interested in type theory, category theory, higher-order logic, and constructive mathematics.

**Conservativity of Type Theory over Higher-order Arithmetic.**

Under Submission.

Coauthor: Benno van den Berg.

paper slides cite

**De Jongh’s Theorem for Type Theory.**

MSc Thesis,*University of Amsterdam*, 2022.

Supervisor: Benno van den Berg.

thesis slides cite**M-types and Bisimulation.**

BSc Thesis,*Leiden University*, 2020

Supervisors: Henning Basold, Peter Bruin.

thesis slides cite

**DutchCATS.***Delft,*6 September 2023.

Talk: Type Checking for Propositional Type Theory in Linear Time. slides**ESSLLI.***Ljubljana,*1–11 August 2023.**CT.***Louvain-la-Neuve,*2–8 July 2023.**Logic PhD-Day.***Groningen,*23 June 2023. organizer**TYPES.***Valentia,*12–15 June 2023.

Talk: Conservativity of Type Theory over Higher-order Arithmetic. slides**The Strength of Weak Type Theory.***Amsterdam,*11–12 May 2023. organizer

Talk: Models for Propositional Type Theory. slides**EuroProofNet WG6**and**HoTT/UF.***Vienna,*22-25 April 2023.**CSL.***Warsaw,*13-16 Februari 2023.**DutchCATS.***Amsterdam*, 16 January 2023.

Talk: Conservativity of the Calculus of Constructions over Higher-order Heyting Arithmetic. slides**The Proof Society Autumn School.***Utrecht,*7-12 November 2022.**Workshop on Algebraic Weak Factorisation Systems.***Amsterdam,*2 May 2022. organizer**DutchCATS***Amsterdam,*27 October 2021.

Talk: M-types and Bisimulation. slides**TYPES.***Online,*14–18 June 2021.

Talk: M-types and Bisimulation. slides

Spring 2023 | Shelah’s eventual Categoricity Conjecture. Organisors: Rodrigo Almeida, Lingyuan Ye. This reading group, framed as a quest to understand Espindola’s proof of Shelah’s eventual categoricty conjecture, is focused on the study of categorical model theory. Topics include: categorical logic, infinitary logic, and topos-theoretic completeness theorems. |

Winter 2022 | What makes Logics (Un)decidable? Supervisor: Balder ten Cate. A project to understand decidability results for modal logic, monadic second-order logic, the guarded fragment, and fixedpoint logic. Talk: Fixedpoint Logic, with Lide Grotenhuis. slides |

Fall 2021 | Set Theory Student Seminar Organisor: Rodrigo Almeida. A seminar by and for master students on various set theoretic topics. Talk: Adding Classes to Set Theory: ZFC ⊆ NBG ⊆ MK. slides |

Summer 2021 | Formalising Effective Kan Fibrations. Supervisors: Benno van den Berg, Eric Faber. We formalised the results of a paper by Benno van den Berg and Eric Faber. This work is motivated by applications in homotopy theory and univalent type theory. |

Winter 2021 | Advanced Set Theory: Forcing and Independence Proofs. Supervisor: Yurii Khomskii. We studied a proof for the independence of the continuum hypothesis in set theory: by constructing models for both ZFC + CH and ZFC + ¬CH. Talk: Forcing ¬CH, with Lide Grotenhuis. slides |

Since 2022 | PhD Candidate. ILLC, University of Amsterdam. Supervisors: Benno van den Berg, Herman Geuvers. |

2020–2022 | Master of Logic. University of Amsterdam, cum laude. - Mathematics Track, - Computation Track. |

2016–2020 | Bachelor of Mathematics. Leiden University, cum laude. |

2016–2020 | Bachelor of Computer Science. Leiden University., cum laude. |