I am a postdoctoral researcher in the INRIA research group Deducteam, interested in the foundations and interoperability of automated reasoning tools—particularly bridging set-theoretic and type-theoretic approaches to mathematics.

I build tools that facilitate interoperability between proof assistants, SMT solvers, and other automated reasoning systems. I also maintain the Zed extension for the LambdaPi proof assistant, and an MCP server that allows LLM agents to interact with LambdaPi.

Currently working on two projects on proof system interoperability:

• 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 the draft paper.

• 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.

Working Papers and Drafts

Publications

Software

• eo2lp — OCaml tool translating Eunoia/cvc5 proof systems to LambdaPi.
• pp2lp — OCaml tool translating Atelier B proof traces to LambdaPi. (With CLEARSY, ANR ICSPA.)
• LambdaPi MCP server — Model Context Protocol server allowing LLM agents to interact with LambdaPi.
• zed-lambdapi — Zed editor extension for LambdaPi with LSP and tree-sitter support.
• Isabelle/HOL/GST — Isabelle framework for generalized set theories.

PhD Thesis