I am a PhD student at the Verimag in Grenoble under Pierre Corbineau and Jean-François Monin.

You can see my CV here

Research

My PhD thesis is on Proxy-based Small Inversions, a technique used in Rocq to perform inversion without equality constraints, well suited to dependent programming. You can find a plugin based on this work here.

Publications

• Pierre Corbineau, Basile Gros, Jean-François Monin. Proxy-based small inversions and their automation. Preprint TYPES 2026. HAL
• Pierre Corbineau, Basile Gros, Jean-François Monin. Certified Programming with Dependent Types Made Simple with Proxy-based Small Inversions. The Rocqshop 2025, Pierre Boutry; Loïc Pujet, Sep 2025, Reykjavik, Iceland. HAL
• Basile Gros, Pierre Corbineau, and Jean-François Monin. Proxy-based small inversions: a case study in metacoq programming. In Adrien Guatto and Marie Kerjean, editors, JFLA 2025 - 36es Journées Francophones des Langages Applicatifs, Jan 2025. HAL

Teaching

I was an assistant teacher for two years, teaching practicals of Introduction to logic and automated proving to second year bachelor students.