My picture

I am a second-year PhD student at Inria Paris’ Cambium team, supervised by François Pottier. My research interests are in programming languages, formal verification, and program semantics.

My current PhD project, called Osiris, is to give mechanised formal semantics for Ocaml logo OCaml, and to provide a program logic for these semantics using Iris logo Iris.

I am also curently working with Son Ho on Aeneas, a tool for the formal verification of Rust programs in Lean.

Publications

Formal semantics and Program Logics for a Fragment of OCaml

Remy Seassau, Irene Yoon, Jean-Marie Madiot, François Pottier

ICFP 2025: International Conference on Functional Programming (2025)

Paper DOI Slides Talk Artifact

Pancake: Verified Systems Programming Made Sweeter

Johannes Åman Pohjola, …, Remy Seassau, M. O. Myreen, M. Norrish, G. Heiser

PLOS, Koblenz, Germany (2023)

Paper DOI

Education

I hold a Master’s degree in Computer Science from the University of Oxford (2022-2023)

I hold a Bachelor’s degree in Mathematics and Computer Science from Ecole Polytechnique (2019-2022)

I am currently enrolled as a PhD student at Université Paris Cité, although my office is located at Inria’s Paris Centre.

Research Visits and Internships

During the summer of 2025, I interned at Microsoft logo Microsoft Research in Cambridge (UK) where I worked with Son Ho on the formal verification of unsafe Rust programs.

In 2022, I work as a research assistant with Johannes Åman Pohjola at the Trustworthy Systems group (home of seL4) hosted at UNSW Sydney, Australia. There, I bootstrapped a verified compiler for Pancake using CakeML’s verified compilation toolchain.

CV

You can find my CV here (last updated 17/09/2025).

Teaching