I am a postdoctoral researcher in the Deducteam research group. My research concerns the foundations and interoperability of automated reasoning tools. I am particularly interested in bridging set-theoretic and type-theoretic approaches to foundations.
Active Projects
pp2lp: Supported by the ANR mission ICSPA (2024–present), an OCaml tool translating proof traces from the Predicate Prover used by Atelier-B—an industrial platform for verifying railway and nuclear safety systems—into LambdaPi, developed in collaboration with CLEARSY. For more information, see the following note.
eo2lp: Supported by an Amazon Research Award (2024–2025), an OCaml tool translating proof certificates from the SMT solver cvc5 to LambdaPi. The translation targets Eunoia, a logical framework that encodes cvc5’s proof calculus. See current working draft of the paper.LambdaPi tooling: MCP server allowing LLM agents to interact with LambdaPi (see related talk), and a Zed editor extension with LSP and tree-sitter support.
Publications
Verifying Atelier B's Predicate Prover
Note — 2026
Automatically Translating Proof Systems for SMT Solvers to the λΠ-calculus
Preprint — 2025
Towards a Set-Theoretic Foundation Closer to Mathematical Text
PhD Thesis — 2023
Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories
Conference for Intelligent Computer Mathematics, Tbisili, Georgia (2022)
Generating Custom Set Theories with Non-Set Structured Objects
Conference for Intelligent Computer Mathematics, Timișoara, Romania (2021)
Adding an Abstraction Barrier to ZF Set Theory
Conference for Intelligent Computer Mathematics, Bertinoro, Italy (2020)