Papers

(updated in 2017)

A draft of my PhD dissertation is below.

    • Sharpening Constraint Programming approaches for Bit-Vector Theory by Zakaria Chihani, Bruno Marre, François Bobot, Sébastien Bardin (CPAIOR 2017) [Draft down below]. A complementary tech report can be found at this page.

    • Translating between implicit and explicit versions of proof by Roberto Blanco, Zakaria Chihani, and Dale Miller. CADE-26 (2017). Draft dated 26 Feb 2017.

    • CDCL-inspired Word-level Learning for Bit-vector Constraint Solving by Zakaria Chihani, François Bobot, Sébastien Bardin. Draft of May 2017.

    • Real Behavior of Floating-Point Numbers by Bruno Marre, François Bobot and Zakaria Chihani. (SMT2017)- Draft of May 2017 below.

    • A Semantic Framework for Proof Evidence by Zakaria Chihani, Dale Miller, Fabien Renaud, Journal of Automated Reasoning (JAR 2016), [link to journal][Link to the HAL version (free access to pre-print)].

    • Proof Certificates for Equality Reasoning by Zakaria Chihani and Dale Miller. LSFA 2015: 10th Workshop on Logical and Semantic Frameworks, with Applications. Natal, Brazil. Draft dated 28 October 2015.

    • The Proof Certifier "Checkers" by Zakaria Chihani, Tomer Libal and Giselle Reis. (Tableaux 2015)[ pdf ].

    • Classical polarizations yield double negation translations by Zakaria Chihani, Danko Ilik and Dale Miller. (draft June 2015) [pdf]

    • The Exp-Log Normal Form of Types and Canonical Terms for Lambda Calculus with Sums by Danko Ilik and Zakaria Chihani (draft February 2015) - pdf on arXiv.

    • Checking foundational proof certificates for first-order logic (extended abstract) by Zakaria Chihani, Dale Miller, and Fabien Renaud. Proceedings of PxTP 2013: Proof Exchange for Theorem Proving, 9-10 June 2013, Lake Placid, USA. Version dated 22 April 2013: pdf. Version on HAL.

    • Foundational proof certificates in first-order logic by Zakaria Chihani, Dale Miller, and Fabien Renaud. Proceedings of CADE 2013, LNAI 7898, pp. 162--177 (2013). Version dated 1 April 2013: pdf.

    • A Semantics for Proof Evidence by Zakaria Chihani, Dale Miller, and Fabien Renaud. LIX Colloquium: Theory and Application of Formal Proofs. November 5–7, 2013 (slides)

I am also part of the development team of Checkers - Proof Checker based on Foundational Proof Certificate.