@inproceedings(Assaf15,
 author       = {A. Assaf},
 year         = {2015},
 title        = {A calculus of constructions with explicit subtyping},
 booktitle    = {The 20th International Conference on Types for Proofs and Programs ({TYPES} '14)},
)
@unpublished(AliHOL,
 author       = {A. Assaf and G. Burel},
 year         = {2014},
 title        = {Translating HOL to Dedukti},
 url          = {https://hal.archives-ouvertes.fr/hal-01097412},
)
@article(Blanqui15,
 author       = {F. Blanqui},
 year         = {2015},
 title        = {Termination of rewrite relations on lambda-terms based on Girard's notion of reducibility.},
 journal      = {Theoretical Computer Science},
 note         = {To appear},
)
@inproceedings(Coqine,
 author       = {M. Boespflug and G. Burel},
 year         = {2012},
 title        = {{CoqInE : Translating the calculus of inductive constructions into the $\lambda\Pi $-calculus modulo.}},
 booktitle    = {The Second International Workshop on Proof Exchange for Theorem Proving {(PxTP)}},
)
@misc(Dedukti,
 author       = {M. Boespflug and Q. Carbonneaux and O. Hermant and R. Saillard},
 title        = {Dedukti},
 url          = {http://dedukti.gforge.inria.fr},
)
@inproceedings(Resolution,
 author       = {G. Burel},
 year         = {2013},
 title        = {{A Shallow Embedding of Resolution and Superposition Proofs into the $\lambda$$\Pi$-Calculus Modulo}},
 booktitle    = {The Third International Workshop on Proof Exchange for Theorem Proving {(PxTP '13)}},
)
@unpublished(RaphaelSigma,
 author       = {R. Cauderlier and C. Dubois},
 year         = {2015},
 title        = {{Objects and Subtyping in the $\lambda\Pi $-Calculus Modulo}},
)
@inproceedings(CousineauDowek07,
 author       = {D. Cousineau and G. Dowek},
 year         = {2007},
 title        = {{Embedding Pure Type Systems in $\lambda\Pi $-Calculus Modulo}},
 booktitle    = {The 8th International Conference on Typed Lambda Calculi and Applications {(TLCA '07)}},
 doi          = {10.1007/978-3-540-73228-0\_9},
)
@unpublished(DorraFO,
 author       = {A. Dorra},
 title        = {Equivalence de Curry-Howard entre le lambda-Pi calcul et la logique intuitionniste},
 note         = {Report},
)
@inproceedings(Geuvers92,
 author       = {H. Geuvers},
 year         = {1992},
 title        = {The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi},
 booktitle    = {The Seventh Annual Symposium on Logic in Computer Science {(LICS '92)}},
 doi          = {10.1109/LICS.1992.185556},
)
@article(Miller91alogic,
 author       = {D. Miller},
 year         = {1991},
 title        = {A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification},
 journal      = {Journal of Logic and Computation},
 doi          = {10.1093/logcom/1.4.497},
)
@article(Muller92,
 author       = {F. M{\"{u}}ller},
 year         = {1992},
 title        = {Confluence of the Lambda Calculus with Left-Linear Algebraic Rewriting},
 journal      = {Information Processing Letters},
 doi          = {10.1016/0020-0190(92)90155-O},
)
@article(DBLP:journals/tocl/NanevskiPP08,
 author       = {Aleksandar Nanevski and Frank Pfenning and Brigitte Pientka},
 year         = {2008},
 title        = {Contextual modal type theory},
 journal      = {{ACM} Trans. Comput. Log.},
 volume       = {9},
 number       = {3},
 doi          = {10.1145/1352582.1352591},
)
@inproceedings(Nipkow-LICS-91,
 author       = {T. Nipkow},
 year         = {1991},
 title        = {Higher-Order Critical Pairs},
 booktitle    = {The Sixth Annual Symposium on Logic in Computer Science {(LICS '91)}},
 doi          = {10.1109/LICS.1991.151658},
)
@inproceedings(DBLP:conf/hoa/Oostrom95,
 author       = {V. van Oostrom},
 year         = {1995},
 title        = {Development Closed Critical Pairs},
 booktitle    = {The Second International Workshop on Higher-Order Algebra, Logic, and Term Rewriting, {(HOA '95)}},
 doi          = {10.1007/3-540-61254-8\_26},
)
@inproceedings(DBLP:conf/popl/Pientka08,
 author       = {Brigitte Pientka},
 year         = {2008},
 title        = {A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions},
 booktitle    = {Symposium on Principles of Programming Languages, ({POPL} '08)},
 doi          = {10.1145/1328438.1328483},
)
@inproceedings(IWIL13,
 author       = {R. Saillard},
 year         = {2013},
 title        = {{Towards explicit rewrite rules in the $\lambda$$\Pi$-calculus modulo}},
 booktitle    = {The 10th International Workshop on the Implementation of Logics {(IWIL '13)}},
)