Presentation
Hello everyone! I am Louise Dubois de Prisque, a PhD student member of the Deducteam at the LMF located at the ENS Paris-Saclay.
My supervisors are Chantal Keller and Valentin Blot.
The subject of my thesis is to improve the automation of the Coq proof assistant by writing certifying compositional transformations from the logic of Coq to a simpler logic which can be handled by automatic provers. To achieve this goal, my supervisors, a former postdoc Pierre Vial and me are developing a Coq plugin called Sniper.
Published papers
- Décision de relations inductives pour SMTCoq (démonstration d’un prototype) (at JFLA 2023) (in French), talk here
- Compositional pre-processing for automated reasoning in dependent type theory (at CPP 23) joint work with Valentin Blot, Denis Cousineau, Enzo Crance, Chantal Keller, Assia Mahboubi and Pierre Vial
- Bécassine à la Chasse au Coq (démonstration) (at JFLA 2022) (in French)
- General automation through modular transformations (at PxTP 2021) joint work with Valentin Blot, Chantal Keller and Pierre Vial
Talks
Teaching
- 2022-2023: Compilation, Networks
- 2021-2022: Logic, Compilation, Data Bases (SQL)
- 2020-2021: Logic, OCaml, Algorithmic
- 2017-2018: Mathematics, Philosophy (at high school level)
Master’s Thesis
The link is available here (in French)