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. 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