EXPERIENCE
I'm working on formalizing and improving the OCaml module system. Our approach is largely inspired by the F-ing translation of SML modules in Fω, which we adapt to the OCaml case.
Clément Blaudeau
Hello! I’m currently a PhD student (2021/2024) under the supervision of Didier Rémy and Gabriel Radanne, at Inria Paris (France), in the Cambium team. I’m working on formalizing and improving the OCaml module system.
Contact me at surname.name@inria.fr
RESEARCH INTERESTS
- Strongly typed functional languages
- Module systems
- Initialization in OOP
- PEG parsing
- Proof assistants (Coq, PVS, Isabelle)
PROJECTS
×
02/2021 – Developing
OCaml modules
My PhD work on the OCaml module system.
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
×
02/2020 – Developing
Celsius project
A conceptual framework for safe object initialization.
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]-
A Conceptual Framework for Safe Object Initialization: A Principled and Mechanized Soundness Proof of the Celsius ModelProc. ACM Program. Lang., vol. 6, Oct, 2022
-
OCaml modules: formalization, insights and improvementsMaster's thesis, École polytechnique fédérale de Lausanne, pp. 67, Sep, 2021
-
A Verified Packrat Parser Interpreter for Parsing Expression GrammarsIn Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 3–17, 2020