I work on building correct and reliable software systems using programming language theory, formal methods, and mechanized reasoning. My focus is on the design and verification of type systems, semantics, and compilers, with an emphasis on connecting theory to real, large-scale software implementations.

I recently completed a PhD on dependent types and subtyping, with fully mechanized proofs in Rocq/Coq. My research bridges foundational type theory with practical systems, ranging from verified compilers to concurrent programming abstractions and proof assistants. I am currently transitioning to industry and seeking roles in software engineering, programming languages, compilers, or high-assurance systems.

Selected Work

Definitional Functoriality for Dependent (Sub)Types — ESOP 2024

  • Developed a novel extension of dependent type theory incorporating structural subtyping
  • Produced a large-scale mechanized proof (~26k LOC) in Rocq/Coq
  • Established soundness and consistency through machine-checked reasoning
  • Received Distinguished Artifact Award

arXiv

CakeML — Verified ML Compiler

  • Contributed to a fully verified ML compiler (~1M LOC) in the HOL ecosystem
  • Extended compiler components while preserving end-to-end correctness guarantees
  • Worked on a mature, production-grade formally verified system used in research and tooling

https://cakeml.org/

Multicore OCaml — Reagents Library

  • Designed and contributed to a concurrent programming abstraction library
  • Focused on compositional concurrency primitives with correctness-aware design
  • Participated in early ecosystem development for Multicore OCaml

https://github.com/ocaml-multicore/reagents

Experience

PhD — Programming Languages & Formal Methods

Inria (Prosecco Team), 2020–2025

  • Designed a novel type system for dependent types with subtyping
  • Developed reusable infrastructure for large-scale mechanized proofs
  • Formalized key results in Rocq/Coq with machine-checked correctness guarantees
  • Published research at top-tier programming languages venues (ESOP)

Research Engineer

Inria, 2018–2020

  • Developed formal models and verification tools in the F* ecosystem
  • Worked across multiple proof assistants (Rocq/Coq, Lean, HOL4, F*)
  • Contributed to applied verification efforts and secure systems research

Education

PhD in Computer Science, Université de Montpellier (2025) Thesis: Structural Subtyping in MLTT

MSc & BSc in Computer Science, École Normale Supérieure Focus: Programming languages, compilers, formal methods

Additional Experience

  • Delivered 20+ research talks at international conferences and seminars
  • Supervised research internships and Master’s thesis work
  • Teaching assistant in mathematics and functional programming (Lycée Henri IV, Sorbonne Université)
  • Volunteer coordination and public speaking (Amnesty International France)

Interests

  • Functional programming and type-driven design
  • Programming language theory and semantics
  • Verified and high-assurance software systems
  • Compilers and developer tooling
  • Bridging formal theory with practical systems