Hi ! I am Raphaël, currently a master’s student in computer science at ENS Paris-Saclay. My main interests include Type theory, Logic, Category theory, Proof Assistants and Programming languages.
Feel free to send me an email if you want to chat or collaborate with me on those topics.
Papers
Fuss-free cumulative universes: theory and practice
Conditionally accepted at POPL (2027)
Talks
Cumulative universes in theory and practice
HoTT/UF (2026)
Cumulative universe hierarchies and their equivalence in dependent type theory
TYPES (2026)
Cumulative hierarchies of universes and their equivalence in type theory
Weekly seminar of the CLASH team at Cambridge University (2026)
Internships
University of Cambridge (5 months)
- Under the supervision of Jon Sterling
- Foundational design and implementation of a new proof assistant based on homotopy type theory (“Project Pterodactyl”). Study and implementation of a new presentation for cumulative universes, its relation to datatypes and implications for the implementation of practical systems. Also, I studied cumulativity in infinity-toposes.
Chalmers University of Technology (2 months)
- Under the supervision of Thierry Coquand.
- Proving the equivalence of different presentations of type theory, notably relating Russell and Tarski presentations of cumulative universe hierarchies. More generally, we related generalised algebraic and pure type system formulations of the syntax.
Education
- Master’s degree in Computer Science (MPRI), 2025-2027
- Bachelor in both Mathematics and Computer Science, 2022-2025