E. Brady, C. Mcbride, and J. Mckinna, Inductive Families Need Not Store Their Indices, TYPES, pp.115-129, 2003.
DOI : 10.1007/978-3-540-24849-1_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.3849

C. A?-gman and J. R. Hindley, Combinatory weak reduction in lambda calculus, Theoretical Computer Science, vol.198, issue.1, pp.239-247, 1998.

. Cardelli, An implementation of FSub, Research Report, vol.97, 1993.

J. Cretin, Erasable coercions: a unified approach to type systems, 2014.
URL : https://hal.archives-ouvertes.fr/tel-00940511

J. Cretin and D. Rémy, System F with coercion constraints, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, 2014.
DOI : 10.1145/2603088.2603128
URL : https://hal.archives-ouvertes.fr/hal-00934408

B. Grégoire and X. Leroy, A compiled implementation of strong reduction, ACM SIGPLAN Notices, vol.37, issue.9, pp.235-246, 2002.
DOI : 10.1145/583852.581501

D. Kesner, The Theory of Calculi with Explicit Substitutions Revisited, Computer Science Logic, pp.238-252, 2007.
DOI : 10.1007/978-3-540-74915-8_20
URL : https://hal.archives-ouvertes.fr/hal-00111285

L. Botlan and D. Rémy, MLF: Raising ML to the power of System-F, ICFP'80, 2003.

P. Letouzey, A New Extraction for Coq, TYPES 2002, 2004.
DOI : 10.1007/3-540-39185-1_12
URL : https://hal.archives-ouvertes.fr/hal-00150914

J. C. Mitchell, Polymorphic type inference and containment. Information and Computation, 1988.

B. Nordström, K. Petersson, and J. M. Smith, Programming in Martin-Löfs type theory, 1990.

R. Pollack, Polishing up the tait-martin-lf proof of the church-rosser theorem, 1995.

F. Pottier, A versatile constraint-based type inference system, Nordic Journal of Computing, vol.7, issue.4, pp.312-347, 2000.

V. Simonet and F. Pottier, A constraint-based approach to guarded algebraic data types, ACM Transactions on Programming Languages and Systems, vol.29, issue.1, 2007.
DOI : 10.1145/1180475.1180476

M. Sulzmann, M. M. Chakravarty, S. L. Jones, and K. Donnelly, System F with type equality coercions, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation , TLDI '07, pp.53-66, 2007.
DOI : 10.1145/1190315.1190324
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.125.2364

M. Takahashi, Parallel Reductions in ??-Calculus, Information and Computation, vol.118, issue.1, pp.120-127, 1995.
DOI : 10.1006/inco.1995.1057

D. Vytiniotis and S. P. Jones, Practical aspects of evidence-based compilation in system FC, 2011.

S. Weirich, J. Hsu, and R. A. Eisenberg, System FC with explicit kind equality, ICFP, pp.275-286, 2013.

. Xi, Dependent ML An approach to practical programming with dependent types, Journal of Functional Programming, vol.17, issue.02, pp.215-286, 2007.
DOI : 10.1017/S0956796806006216