A calculus of constructions with explicit subtyping, The 20th International Conference on Types for Proofs and Programs (TYPES '14), 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01097401
Translating HOL to Dedukti Available at https, 2014. ,
Termination of rewrite relations on lambda-terms based on Girard's notion of reducibility. Theoretical Computer Science, 2015. ,
CoqInE : Translating the calculus of inductive constructions into the ? ?calculus modulo, The Second International Workshop on Proof Exchange for Theorem Proving, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-01126128
A Shallow Embedding of Resolution and Superposition Proofs into the ? ?-Calculus Modulo, The Third International Workshop on Proof Exchange for Theorem Proving (PxTP '13), 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-01126321
Objects and Subtyping in the ? ?-Calculus Modulo, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01126394
Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, The 8th International Conference on Typed Lambda Calculi and Applications (TLCA '07), 2007. ,
DOI : 10.1007/978-3-540-73228-0_9
Equivalence de Curry-Howard entre le lambda-Pi calcul et la logique intuitionniste ,
The Church-Rosser property for beta eta -reduction in typed lambda -calculi, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. ,
DOI : 10.1109/LICS.1992.185556
A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, Journal of Logic and Computation, 1991. ,
Confluence of the lambda calculus with left-linear algebraic rewriting, Information Processing Letters, vol.41, issue.6, p.90155, 1992. ,
DOI : 10.1016/0020-0190(92)90155-O
Contextual modal type theory, ACM Transactions on Computational Logic, vol.9, issue.3, 2008. ,
DOI : 10.1145/1352582.1352591
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1028.3796
Higher-order critical pairs, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, 1991. ,
DOI : 10.1109/LICS.1991.151658
Development closed critical pairs, 1995. ,
DOI : 10.1007/3-540-61254-8_26
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions, Symposium on Principles of Programming Languages, 2008. ,
Towards explicit rewrite rules in the ? ?-calculus modulo, The 10th International Workshop on the Implementation of Logics (IWIL '13), 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00921340