user_image

Clément Blaudeau

Hello! I’m a Proof Engineer at Cryspen, working on a the Hax toolchain that translates Rust code to various proof assistants. My work involves tooling, proof engineering, and proving cryptographic rust code correct, mainly using Lean and F★.

Previously, I did my PhD (2021-2024) at Inria Paris in the Cambium team, where I formalized the typing system of the OCaml module layer under the supervision of Didier Rémy and Gabriel Radanne. Contact me at surname at cryspen dot com

EXPERIENCE

  • 2025-05-01 – present

    Proof Engineer, Cryspen

  • 2021-10-01 – 2024-12-31

    PhD, Inria (France)

  • 2019-09-01 – 2021-06-01

    Computer Science Master, EPFL (Switzerland)

  • 2016-09-01 – 2021-06-01

    Engineering degree, Ecole polytechnique (France)

RESEARCH INTERESTS

  • Formal verification of software
  • Proof engineering (Lean, Rocq, PVS)
  • Rust ecosystem, tooling and compiler
  • Type systems
  • Modularity
  • Functional programming
  • Initialization of recursive structures
  • PEG parsing

PROJECTS

Logo of the OCaml language

02/2022 – Developing

Momega: OCaml modules, the F-omega way
I'm working on formalizing and improving the OCaml module system. Our approach is largely inspired by F-ing modules (Rossberg & al), which I extended with transparent existentials. Right now, we're focusing on complex type definitions (GADTs, extensible types, parametric types, variance, etc.) abstract signatures and recursive modules! See our OOPSLA2024 paper for more details
Logo of the OCaml language

02/2024 – Developing

ZipML: OCaml modules, the syntactic way
In parallel, I'm also working on a syntactic type system, more aimed at real world implementations. It solves the signature avoidance problem with a new notion of zipper signatures, and has a bunch of nice features. You can see our draft (under revision) by clicking on the eye button below
Logo of the Celsius project

02/2022 – Developing

Celsius project
Initialization of objects is a tricky subject in OOP: objects under initialization do not satisfy their class specification yet, and are thus unsafe to use. In this project I developed the Coq formalization of the Celsius language, a light typing annotation system that ensures safe initialization. You can look at the OOPSLA 2022 paper or the associated Coq project. This work was done with Fengyun Liu, as an continuation of his thesis

RECENT PUBLICATIONS

[All Publications]
  1. Avoiding Signature Avoidance in ML Modules with Zippers
    Blaudeau, Clément, Rémy, Didier, and Radanne, Gabriel
    Proceedings of the ACM on Programming Languages, vol. POPL, no. 9, Jan, 2025
  2. Fulfilling OCaml Modules with Transparency
    Clement, Blaudeau, Rémy, Didier, and Radanne, Gabriel
    Proc. ACM Program. Lang., vol. 8, no. OOPSLA1, Apr, 2024
  3. A Conceptual Framework for Safe Object Initialization: A Principled and Mechanized Soundness Proof of the Celsius Model
    Blaudeau, Clément, and Liu, Fengyun
    Proc. ACM Program. Lang., vol. 6, no. OOPSLA2, Oct, 2022