The λΠ-calculus Modulo as a Universal Proof Language. - Mathieu Boespflug; Quentin Carbonneaux; Olivier Hermant (PxTP, 2012)

Envy-free two-player mm-cake and three-player two-cake divisions. - Nicolas Lebert; Frédéric Meunier; Quentin Carbonneaux (Oper. Res. Lett., 2013)

End-to-end verification of stack-space bounds for C programs. - Quentin Carbonneaux; Jan Hoffmann 002; Tahina Ramananandro; Zhong Shao 001 (PLDI, 2014)

Compositional certified resource bounds. - Quentin Carbonneaux; Jan Hoffmann 002; Zhong Shao 001 (PLDI, 2015)

Automated Resource Analysis with Coq Proof Objects. - Quentin Carbonneaux; Jan Hoffmann 002; Thomas W. Reps; Zhong Shao 001 (CAV (2), 2017)

Bounded expectations: resource analysis for probabilistic programs. - Van Chan Ngo; Quentin Carbonneaux; Jan Hoffmann 002 (PLDI, 2018)

Applying formal verification to microkernel IPC at meta. - Quentin Carbonneaux; Noam Zilberstein; Christoph Klee; Peter W. O'Hearn; Francesco Zappa Nardelli (CPP, 2022)

SWE-RL: Advancing LLM Reasoning via Reinforcement Learning on Open Software Evolution. - Yuxiang Wei 003; Olivier Duchenne; Jade Copet; Quentin Carbonneaux; Lingming Zhang 001; Daniel Fried; Gabriel Synnaeve; Rishabh Singh; Sida I. Wang (CoRR, 2025)

What I cannot execute, I do not understand: Training and Evaluating LLMs on Program Execution Traces. - Jordi Armengol-Estapé; Quentin Carbonneaux; Tianjun Zhang; Aram H. Markosyan; Volker Seeker; Chris Cummins; Melanie Kambadur; Michael F. P. O'Boyle; Sida I. Wang; Gabriel Synnaeve; Hugh James Leather (CoRR, 2025)