Mohamed Yacine EL HADDAD

LSV, CNRS & ENS Paris-Saclay
~~61, avenue du Président Wilson~~ 4, avenue des sciences
~~94235 CACHAN Cedex, France~~ 91190 Gif-sur-Yvette
elhaddad [at] lsv . fr
Office : ~~C1-13~~ 3 S 64
Phone : ~~+33 (0)1 47 40 77 82~~ +33 (0) 1 81 87 54 71

I'm currently a PhD Student at LSV (Laboratoire Spécification et Vérification) under the supervision of Frédéric Blanqui and Guillaume Burel. I'm working on Integrating Automated Provers in Proof Assistants, a project funded by DigiCosme and LSV . Click here for more information about my thesis.

Research

Papers

ekstrakto, a tool to reconstruct Dedukti proof from TSTP files, with Guillaume Burel and Frédéric Blanqui , 9 pages, PxTP'19, to appear in EPTCS 301 (PDF).

Software

Ekstrakto : a TSTP to Dedukti translator.
Dedukti : an universal proof checker.
Lambdapi : an extension of Dedukti with metavariables and tactics.
Zenon Modulo : a first-order automated theorem prover based on the tableau method.

Talks

Integrating Automated Provers in Proof Assistants.(Slides)

Barbizon, June 2018
Integrating Automated Provers in Proof Assistants.(Slides & Poster)

SAMOVAR, November 2018
ekstrakto, a tool to reconstruct Dedukti proof from TSTP files.(Slides)

Natal-Brazil, August 2019

Experience

Junior Researcher

CNRS

January 2018 - Now

Web Master

Merid Technology

June 2017 - January 2018

Web Developer

Media Labs

January 2017 - June 2017

Education

University of Paris-Saclay

PhD Student

Sciences et technologies de l'information et de la communication

More information about my thesis.

January 2018 - Now

University of Boumerdes

Master's degree

Computer Science - Software Engineering and Information Processing

Report (in french)

September 2014 - August 2016

University of Boumerdes

Bachelor's degree

Computer Science

September 2011 - July 2014