user_image

Clément Blaudeau

Hello! I’m a 3rd year PhD student (2021/2024) at Inria Paris (France), in the Cambium team. I’m working on formalizing and improving the typing of the OCaml module system, under the supervision of Didier Rémy and Gabriel Radanne. Contact me at surname dot name at inria.fr

EXPERIENCE

  • 2021-10-01 – 2024-10-01

    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

  • Type systems
  • Modularity
  • Initialization of recursive structures
  • PEG parsing
  • Proof assistants (Coq, PVS, Isabelle)

PROJECTS

Logo of the OCaml language

02/2021 – Developing

OCaml modules
I'm working on formalizing and improving the OCaml module system. Our approach is largely inspired by the F-ing modules (Rossberg & al), which we adapt to the OCaml case. You can look at our draft (accepted at OOPSLA 2024) paper by clicking on link below
Logo of the Celsius project

02/2020 – 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. 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, Oct, 2022
  2. OCaml modules: formalization, insights and improvements
    Blaudeau, Clément
    Master's thesis, École polytechnique fédérale de Lausanne, pp. 67, Sep, 2021
  3. A Verified Packrat Parser Interpreter for Parsing Expression Grammars
    Blaudeau, Clement, and Shankar, Natarajan
    In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 3–17, 2020