Translating HOL to Dedukti A Assaf, G Burel Proof Exchange for Theorem Proving, 2015 | 36 | 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 | 25 | 2014 |
A Calculus of Constructions with explicit subtyping A Assaf Types for Proofs and Programs, 2014 | 25 | 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 |