A. Abel, Implementing a normalizer using sized heterogeneous types, Journal of Functional Programming, vol.19, issue.3-4, 2006.
DOI : 10.1017/S0956796807006430

A. Abel and T. Altenkirch, A predicative analysis of structural recursion, Journal of Functional Programming, vol.12, issue.01, pp.1-41, 2002.
DOI : 10.1017/S0956796801004191

A. Abel and D. Rodriguez, Syntactic Metatheory of Higher-Order Subtyping, Lecture Notes in Computer Science, vol.5213, pp.446-460, 2008.
DOI : 10.1007/978-3-540-87531-4_32

T. Altenkirch and J. Chapman, Tait in one big step, Workshop on Mathematically Structured Functional Programming, 2006.

T. Altenkirch and B. Reus, Monadic Presentations of Lambda Terms Using Generalized Inductive Types, Lecture Notes in Computer Science, vol.1683, pp.453-468, 1999.
DOI : 10.1007/3-540-48168-0_32

N. Benton, A. Kennedy, and C. Hur, Strongly Typed Term Representations in Coq, Journal of Automated Reasoning, vol.14, issue.1
DOI : 10.1007/s10817-011-9219-0

K. Crary, Explicit Contexts in LF (Extended Abstract), Electronic Notes in Theoretical Computer Science, vol.228, pp.53-68, 2009.
DOI : 10.1016/j.entcs.2008.12.116

R. David, Normalization without reducibility. Annals of pure and applied logic, pp.121-130, 2001.
DOI : 10.1016/s0168-0072(00)00030-0
URL : https://hal.archives-ouvertes.fr/hal-00384697

N. G. De-bruijn, Lambda Calculus Notation with Nameless Dummies: a Tool for Automatic Formula Manipulation With Application to the Church-Rosser Theorem, Indag. Math, pp.381-382, 1972.

R. Harper and D. R. Licata, Mechanizing metatheory in a logical framework, Journal of Functional Programming, vol.40, issue.4-5, pp.613-673, 2007.
DOI : 10.1006/inco.2001.2951

F. Pfenning, Church and Curry: Combining intrinsic and extrinsic typing, Studies in Logic and the Foundations of Mathematics, 2008.

B. Pientka, A type-theoretic foundation for programming with higherorder abstract syntax and first-class substitutions, POPL, pp.371-382, 2008.

B. Pierce, Types and programming languages, 2002.

K. Watkins, I. Cervesato, F. Pfenning, and D. Walker, A Concurrent Logical Framework: The Propositional Fragment, Lecture Notes in Computer Science, vol.3085, pp.355-377, 2003.
DOI : 10.1007/978-3-540-24849-1_23