I am a PhD candidate working in the EPICURE team at Inria Rennes. My supervisors are Sandrine Blazy and Frédéric Besson.

My PhD thesis is about Barocq, a restricted, first-order, purely functional language compiled to efficient C code. The purpose of Barocq is to write system software (e.g, microkernel) in a functional style, to reason about it in the Rocq proof assistant, whilst enjoying its “optimising” compiler that generates C programs that do not require dynamic memory allocation.

From April to June 2025, I was a visiting PhD student at KTH Royal Institute of Technology in Stockholm. I worked with Roberto Guanciale and Henrik Karlsson on the re-implementation of the S3K microkernel in Barocq.

Formerly, I was an intern at Inria Rennes under the supervision of Frédéric Besson and Tristan Ninet. I worked on a verified compiler for a packet filtering language.

Publications

  • Towards Verifiable System Code using a DSL Compiled to Efficient and Readable C Code, at LCTES’26. markdown language Best paper award
    Clément Chavanon, Henrik Karlsson, Frédéric Besson, Sandrine Blazy, Roberto Guanciale.
    Proceedings of the 27th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2026). [doi] [preprint] [talk].

  • PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams, at CPP’24.
    Clément Chavanon, Frédéric Besson, Tristan Ninet.
    Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024). [doi] [preprint] [talk].

Teaching assistance

2025 - 2026

  • PRGC (Programmation de confiance - Trustworthy programming), L3 ISTIC, University of Rennes.
    Lecturer: Sandrine Blazy.
  • Programmation fonctionnelle - Functional programming, 3INFO, INSA Rennes.
    Lecturer: Frédéric Besson.

2024 - 2025

  • PRGC (Programmation de confiance - Trustworthy programming), L3 ISTIC, University of Rennes.
    Lecturer: Sandrine Blazy.
  • Programmation fonctionnelle - Functional programming, 3INFO, INSA Rennes.
    Lecturer: Frédéric Besson.

2023 - 2024

  • PRGC (Programmation de confiance - Trustworthy programming), L3 ISTIC, University of Rennes.
    Lecturer: Sandrine Blazy.
  • Programmation fonctionnelle - Functional programming, 3INFO, INSA Rennes.
    Lecturer: Frédéric Besson.
  • ACE (Algorithmique et Complexité Expérimentale - Algorithmics and Complexity Analysis), L1 ISTIC, University of Rennes.
    Lecturer: Thomas Genet.