I am a researcher at Inria in the PICUBE team at the IRIF laboratory. My research focuses on generative AI for interactive theorem proving (agent-prover interfaces, tools, specialized models), and on probabilistic programming languages (language design, semantics, static analysis, compilation, inference).
Since 2024, I have co-led the Inria Défi LLM4Code, and I started LLM4Rocq research group. From 2020 to 2023 I was a member of the PARKAS team at the Département d'Informatique (DI) of the École normale supérieure (ENS). From 2017 to 2020 I was a research staff member at the IBM T.J. Watson Research Center in the AI Programming Models team.
News
- Aug 2026 small-prime-gap (with A. Mahboubi), a Rocq mechanisation of the computer-aided step of Prop. 4.3(2) in Maynard's “Small gaps between primes”, accepted at AITP 2026.
- Jul 2026 “PPDL: LLM-Based Flows as Probabilistic Programs” (with L. Mandel, M. Vaziri, M. Hirzel) presented at ICML 2026 (main track), and “Library Before Proof” (with M. Lelarge) at AI4Research@ICML 2026.
- Jun 2026 Putnam 2025 in Rocq: all twelve problems closed, 12/12 verified.
Services
| Organizer | EPIT 2026 (co-chair), OOPSLA 2024 AEC (co-chair), OOPSLA 2023 ERC-AEC (co-chair), IBM PL Day 2019 (co-chair), DEBS 2019 industry (chair), IBM PL Day 2018 (co-chair) |
|---|---|
| PC Member | AITP 2026, OOPSLA 2025, JFLA 2025, JFLA 2024, FDL 2023, LCTES 2023, LAFI 2023, REBLS 2022, REBLS 2021, EMSOFT 2021, DEBS 2021 industry, LCTES 2021, CC 2021, FDL 2020, EMSOFT 2020, LCTES 2020, DEBS 2020 industry, REBELS 2019, EMSOFT 2019, DEBS 2018, DLS 2017 |
| Reviewer | MathAI@NeurIPS 2026, NeurIPS 2026, ICML 2026, OOPSLA 2026, CPP 2026, POPL 2026, ACM TECS 2024, ACM TSE 2023, IEEE TCAD 2020, ACM TECS 2020, EMSOFT 2016, EMSOFT 2015, DAC 2015, JFLA 2015, JFLA 2014 |
Software
| rocq-mcp | MCP server for the Rocq prover (OCaml/Python) |
|---|---|
| mathcomp-skills | Agent skills for writing idiomatic MathComp code (Rocq/Doc) |
| pytanque | Python API for lightweight communication with Rocq (OCaml/Python) |
| probzelus | Compiler and runtime for a synchronous probabilistic language (OCaml/Zelus) |
| dppl | Compiler from Stan++ to Pyro (OCaml/Python) |
| lale | A library for semi-automated data science (Python) |
Awards
- FDL 2023, Outstanding Reviewer Award
- ISSTA 2022, ACM SIGSOFT Distinguished Paper Award
- ESEC/FSE 2020, ACM SIGSOFT Distinguished Paper Award
- ACM SIGBED 2017, Paul Caspi Memorial Dissertation Award
- FDL 2017, Best Paper Award
- EMSOFT 2016, Best Paper Nominee
- EMSOFT 2013, Best Paper Nominee
- EMSOFT 2013, Student Travel Grant