A framework for defining computational higher-order logicsnew
École Polytechnique, 2015, Paris
[ pdf | hal | slides ]
Supervisors: G. Dowek and G. Burel
Publications
Mixing HOL and Coq in Dedukti
A. Assaf and R. Cauderlier
Fourth Workshop on Proof Exchange for Theorem Proving, PxTP 2015
[ pdf | slides ]
Translating HOL Light to Dedukti
A. Assaf and G. Burel
Fourth Workshop on Proof Exchange for Theorem Proving, PxTP 2015
[ pdf | slides ]
Conservativity of embeddings in the λΠ-calculus modulo rewriting
A. Assaf
13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015
[ pdf | slides ]
A calculus of constructions with explicit subtyping
A. Assaf
20th International Conference on Types for Proofs and Programs, TYPES 2014
[ pdf | drops ]
Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus
A. Assaf, A. Diaz-Caro, S. Perdrix, C. Tasson, and B. Valiron
In Logical Methods in Computer Science, volume 10, issue 4, 2014
[ pdf | arXiv ]
Completeness of algebraic CPS simulations
A. Assaf and S. Perdrix
I7th International Workshop on Developments of Computational Methods, DCM 2011
[ pdf | arXiv ]
Master’s thesis
Traduction de HOL en Dedukti
École Polytechnique, 2012, Paris
[ pdf ]