Mohamed Yacine EL HADDAD

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

Education