Completeness of algebraic CPS simulations - Ali Assaf 002; Simon Perdrix (DCM, 2011)

A Calculus of Constructions with Explicit Subtyping. - Ali Assaf 002 (TYPES, 2014)

Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus - Ali Assaf 002; Alejandro Díaz-Caro; Simon Perdrix; Christine Tasson; Benoît Valiron (Log. Methods Comput. Sci., 2014)

Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting. - Ali Assaf 002 (TLCA, 2015)

Translating HOL to Dedukti. - Ali Assaf 002; Guillaume Burel (PxTP@CADE, 2015)

Mixing HOL and Coq in Dedukti (Extended Abstract). - Ali Assaf 002; Raphaël Cauderlier (PxTP@CADE, 2015)

Conservativity of embeddings in the lambda Pi calculus modulo rewriting (long version). - Ali Assaf 002 (CoRR, 2015)

A framework for defining computational higher-order logics. (Un cadre de définition de logiques calculatoires d'ordre supérieur). - Ali Assaf 002 (2015)

Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. - Ali Assaf 002; Guillaume Burel; Raphaël Cauderlier; David Delahaye; Gilles Dowek; Catherine Dubois; Frédéric Gilbert 002; Pierre Halmagrand; Olivier Hermant; Ronan Saillard (CoRR, 2023)