Jérémy Thibault

Curriculum Vitae

My CV is available in English (long version) and in French (long version)

Publications

Conferences

• 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

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, publications under review

• Jérémy Thibault and Clément Pit-Claudel.
  “Verified Compilation Modulo Custom Type and Function Implementations in Rocq,” 2026.
  • Currently under review
  • 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.
• 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
• 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).