Jérémy Thibault

Curriculum Vitae

My CV is available in English in French.

Publications

Conferences

• Jérémy Thibault and Clément Pit-Claudel.
  “Verified Compilation Modulo Custom Type and Function Implementations in Rocq,” 2026.
  • Accepted at CPP'27
  • Summary: we describe a technique to build verified compilers that support custom type implementations, and we apply it to two verified extraction pipelines for Rocq.
• Jérémy Thibault, Joseph Lenormand, and Catalin Hritcu.
  “Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs,”
  in 16th International Conference on Interactive Theorem Proving, ITP 2025, September 28 to October 1, 2025, Reykjavik, Iceland,
  ed. Yannick Forster and Chantal Keller, vol. 352, LIPIcs (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025), 29:1–20, https://doi.org/10.4230/LIPICS.ITP.2025.29.
  • Rocq development
• Jérémy Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, Aïna Linn Georges, Cătălin Hriţcu, and Andrew Tolmach.
  “SECOMP: Formally Secure Compilation of Compartmentalized c Programs,”
  in Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, CCS ’24 (ACM, 2024), 1061–75, https://doi.org/10.1145/3658644.3670288.
  • Rocq development
• Akram El-Korashy, Roberto Blanco, Jérémy Thibault, Adrien Durier, Deepak Garg, and Cătălin Hriţcu.
  “SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation,”
  in 2022 IEEE 35th Computer Security Foundations Symposium (CSF) (IEEE, 2022), 64–79, https://doi.org/10.1109/csf54842.2022.9919680.
  • Rocq development
• Carmine Abate, Roberto Blanco, Ștefan Ciobâcă, Adrien Durier, Deepak Garg, Cătălin Hrițcu, Marco Patrignani, Éric Tanter, and Jérémy Thibault.
  “Trace-Relating Compiler Correctness and Secure Compilation,”
  in Programming Languages and Systems (Springer International Publishing, 2020), 1–28, https://doi.org/10.1007/978-3-030-44914-8_1.
  • Superseded by An Extended Account of Trace-relating Compiler Correctness and Secure Compilation
  • Rocq development
• Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and Jérémy Thibault.
  “Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation,”
  in 2019 IEEE 32nd Computer Security Foundations Symposium (CSF) (IEEE, 2019), https://doi.org/10.1109/csf.2019.00025.
  • Distinguished Paper Award
  • Rocq development

Conference submissions (under review)

• Basile Schlosser, Jérémy Thibault, and Catalin Hritcu.
  “Blame-Aware Recomposition for Secure Compilation Proofs of Low-Level Compartment Isolation,” 2026, https://arxiv.org/abs/2610.26054.
  • Currently under review
  • Rocq development

Journals

• Carmine Abate, Roberto Blanco, Ştefan Ciobâcă, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, and Jérémy Thibault.
  “An Extended Account of Trace-Relating Compiler Correctness and Secure Compilation,”
  ACM Trans. Program. Lang. Syst. 43, no. 4 (2021): 14:1–48, https://doi.org/10.1145/3460860.
  • Supersedes Trace-Relating Compiler Correctness and Secure Compilation
  • Rocq development

Informal publications

• Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Catalin Hritcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, Jérémy Thibault, and Andrew Tolmach.
  “When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise,” 2019, https://arxiv.org/abs/1802.00588.
  • Rocq development
  • Contribution: significant improvement to the proof by removing the use of partial semantics

Service

Conference PC

• CSF'27

Workshop PC

• PriSC'26
• PriSC'25

Artifact evaluation committee

• OOPSLA'24, POPL'23

Teaching

• Instructor for CS-428 (Interactive Theorem Proving) (Spring 2026, EPFL, Switzerland).
  Master-level course on interactive theorem proving, computer-checked mathematics, compiler verification, proofs as programs, dependent types, and proof automation.

• Teaching assistant for Foundations of Programming Languages, Verification, and Security (Winter Semester 2023-2024, Ruhr Universität Bochum, Germany).
  One semester course based on Software Foundations Vol. 2.

• Teaching assistant for Writing and Verifying Functional Programs in Coq (Summer School on Cryptography, Blockchain, and Program Verification, Mathinfoly 2019, Lyon, France).

Internships

• Internship in the Prosecco Team at Inria.
  Subject: “A Trace-based Proof Technique for Secure Compilation”.
  • Supervision: Cătălin Hriţcu.
  • From February 2018 to June 2018
  • The work was integrated in our paper, Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation
• Internship in the Logic and semantics group at Aarhus University.
  Subject: “Improving language-based predictive mitigation for information-flow security"
  • Supervision: Aslan Askarov.
  • From June 2017 to August 2017
  • Internship report: Improving language-based predictive mitigation for information-flow security.
• Internship in the SUMO Team at Irisa (Rennes, France).
  Subject: «Games with hierarchical objectives»
  • Supervision: Ocan Sankur
  • From May 2016 to July 2016