I am a postdoctoral researcher at the Laboratoire Méthodes Formelles (LMF) at ENS Paris-Saclay, working within the research group Deducteam.
I am interested in mathematical and computational structures for representing mathematics. In particular, I have a special interest in the intersection of type-theoretic and set-theoretic technqiues for interactive theorem proving.
Currently, I’m working on translating specifications and proofs from SMT solvers (in particular, cvc5) to the proof assistant Lambdapi.
Publications
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, Temasora, Italy (2020)