I am a Phd student at Inria Nancy in the VeriDis team and I’m part of the Matryoshka project. The main goal of my Phd is to design a higher-order SMT-solver. My supervisors are Pascal Fontaine and Jasmin Christian Blanchette. I’m graduated of MSc degree in Computer Sciences from (MPRI) at University of Paris Diderot in 2017.


Higher-order SMT solving (work in progress)

Haniel Barbosa, Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui, and Cesare Tinelli. In Dimitrova, R., D’Silva, V. (eds.), 16th International Workshop on Satisfiability Modulo Theories (SMT 2018). Preprint (PDF)

Language and proofs for higher-order SMT (work in progress)

Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, and Pascal Fontaine. Accepted at 5th Workshop on Proof eXchange for Theorem Proving (PxTP 2017). Preprint (PDF)

Proof in Coq of the IE property for the Linear Substitution (Ls)

Code here
This is a formalization of the proof of Beniamino Accattoli of the preservation of the strong normalization of linear substitution realized in L3 and M1 internships, at the LIPN. My advisors were Micaela Mayero and Damiano Mazza. For more details you may look in the unpublished article about this formalization here