| Translating HOL to Dedukti A Assaf, G Burel Proof Exchange for Theorem Proving, 2015 | 37 | 2015 |
| Call-by-value, call-by-name and the vectorial behaviour of the algebraic lambda-calculus A Assaf, A Díaz-Caro, S Perdrix, C Tasson, B Valiron Logical Methods in Computer Science, 2014 | 27 | 2014 |
| A Calculus of Constructions with explicit subtyping A Assaf Types for Proofs and Programs, 2014 | 26 | 2014 |
| Conservativity of embeddings in the lambda-Pi calculus modulo rewriting A Assaf Typed Lambda Calculi and Applications, 2015 | 12 | 2015 |
| Completeness of algebraic CPS simulations A Assaf, S Perdrix Developments of Computational Models, 2011 | 6 | 2011 |
| Mixing HOL and Coq in Dedukti (Rough Diamond) A Assaf, R Cauderlier Interactive Theorem Proving, 2015 | 1 | 2015 |
| Traduction de HOL en Dedukti A Assaf Master Parisien de Recherche en Informatique (MPRI), École Polytechnique, 2012 | 1 | 2012 |
