Translating HOL to Dedukti A Assaf, G Burel Proof Exchange for Theorem Proving, 2015 | 34 | 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 | 22 | 2014 |

A Calculus of Constructions with explicit subtyping A Assaf Types for Proofs and Programs, 2014 | 21 | 2014 |

Conservativity of embeddings in the lambda-Pi calculus modulo rewriting A Assaf Typed Lambda Calculi and Applications, 2015 | 10 | 2015 |

Completeness of algebraic CPS simulations A Assaf, S Perdrix Developments of Computational Models, 2011 | 7 | 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 |