. Proof, By induction on the constructions of

A. Abel, Semi-continuous sized types and termination, Logical Methods in Computer Science, vol.4, issue.2, 2008.
DOI : 10.2168/lmcs-4(2:3)2008

URL : http://arxiv.org/abs/0804.0876

A. Abel and . Miniagda, Integrating sized and dependent types, Workshop on Partiality And Recursion in Interative Theorem Provers, 2010.

P. Aczel, An Introduction to Inductive Definitions, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pp.739-782, 1977.
DOI : 10.1016/S0049-237X(08)71120-0

P. Aczel, On Relating Type Theories and Set Theories, Types for Proofs and Programs, International Workshop TYPES '98, pp.1-18, 1998.
DOI : 10.1007/3-540-48167-2_1

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.2658

R. Adams, Pure type systems with judgemental equality, Journal of Functional Programming, vol.16, issue.02, pp.219-246, 2006.
DOI : 10.1017/S0956796805005770

T. Altenkirch, Constructions, Inductive Types and Strong Normalization, 1993.

T. Altenkirch, C. Mcbride, and J. Mckinna, Why dependent types matter . Manuscript, available online, 2005.

R. M. Amadio, Held as Part of the Joint European Conferences on Theory and Practice of Software, 11th International Conference Proceedings, volume 4962 of Lecture Notes in Computer Science, 2008.

L. Augustsson, Cayenne -a language with dependent types, Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, ICFP '98, pp.239-250, 1998.

H. Barendregt, Lambda calculi with types, Handbook of Logic in Computer Science, pp.117-309, 1992.
DOI : 10.1017/cbo9781139032636

B. Barras, Auto-validation d'un système de preuves avec familles inductives, Thèse de doctorat, 1999.

B. Barras, Sets in Coq, Coq in sets, 1st Coq Workshop, 2009.

B. Barras and B. Bernardo, The Implicit Calculus of Constructions as a Programming Language with Dependent Types, Amadio [9], pp.365-379
DOI : 10.1007/978-3-540-78499-9_26

URL : https://hal.archives-ouvertes.fr/inria-00429543

B. Barras, P. Corbineau, B. Grégoire, H. Herbelin, and J. L. Sacchini, A New Elimination Rule for the Calculus of Inductive Constructions, Berardi et al. [22], pp.32-48
DOI : 10.1007/978-3-540-74464-1_16

URL : https://hal.archives-ouvertes.fr/inria-00524938

G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu, Type-based termination of recursive definitions, Mathematical Structures in Computer Science, vol.14, issue.1, pp.97-141, 2004.
DOI : 10.1017/S0960129503004122

G. Barthe, B. Grégoire, and F. Pastawski, Practical Inference for Type-Based Termination in a Polymorphic Setting, Typed Lambda Calculi and Applications, 7th International Conference Proceedings, pp.71-85, 2005.
DOI : 10.1007/11417170_7

G. Barthe, B. Grégoire, and F. Pastawski, CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions, Hermann and Voronkov [46], pp.257-271
DOI : 10.1007/11916277_18

G. Barthe, B. Grégoire, and C. Riba, A Tutorial on Type-Based Termination, Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School, pp.100-152, 2008.
DOI : 10.1023/A:1019916231463

G. Barthe, B. Grégoire, and C. Riba, Type-Based Termination with Sized Products, Computer Science Logic, 22nd International Workshop 17th Annual Conference of the EACSL, pp.493-507, 2008.
DOI : 10.1007/978-3-540-87531-4_35

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development . Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
DOI : 10.1007/978-3-662-07964-5

URL : https://hal.archives-ouvertes.fr/hal-00344237

Y. Bertot and E. Komendantskaya, Using Structural Recursion for Corecursion, Berardi et al. [22], pp.220-236
DOI : 10.1007/BFb0105417

URL : https://hal.archives-ouvertes.fr/inria-00322331

F. Blanqui, A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems, Rewriting Techniques and Applications, 15th International Conference Proceedings, pp.24-39, 2004.
DOI : 10.1007/978-3-540-25979-4_2

URL : https://hal.archives-ouvertes.fr/inria-00100254

F. Blanqui and C. Riba, Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems, Hermann and Voronkov [46], pp.105-119
URL : https://hal.archives-ouvertes.fr/inria-00084837

A. Bove, General Recursion in Type Theory, Geuvers and Wiedijk, pp.39-58
DOI : 10.1007/3-540-39185-1_3

T. Coquand, Metamathematical investigations of a calculus of constructions, Logic and computer science, pp.91-122, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00075471

T. Coquand, Pattern matching with dependent types, Informal Proceedings Workshop on Types for Proofs and Programs, 1992.

T. Coquand, Infinite objects in type theory, Barendregt and Nipkow [12], pp.62-78
DOI : 10.1007/3-540-58085-9_72

T. Coquand and G. Huet, The calculus of constructions, Information and Computation, vol.76, issue.2-3, pp.95-120, 1988.
DOI : 10.1016/0890-5401(88)90005-3

URL : https://hal.archives-ouvertes.fr/inria-00076024

T. Coquand and C. Paulin, Inductively defined types, COLOG-88, International Conference on Computer Logic Proceedings, pp.50-66, 1988.
DOI : 10.1007/3-540-52335-9_47

R. Pollack, The LEGO Proof Assistant, 2001.

M. Frade, Type-Based Termination of Recursive Definitions and Constructor Subtyping in Typed Lambda Calculi, 2003.

H. Geuvers and M. Nederhof, Modular proof of strong normalization for the calculus of constructions, J. Funct. Program, vol.1, issue.2, pp.155-189, 1991.

H. Geuvers and F. Wiedijk, The Netherlands, Types for Proofs and Programs, Second International Workshop, 2002.

E. Giménez, Codifying guarded definitions with recursive schemes, Types for Proofs and Programs, International Workshop TYPES'94, pp.39-59, 1994.
DOI : 10.1007/3-540-60579-7_3

E. Giménez, A Calculus of Infinite Constructions and its application to the verification of communicating systems, 1996.

E. Giménez, Structural recursive definitions in type theory, Automata, Languages and Programming , 25th International Colloquium, ICALP'98 BIBLIOGRAPHY Proceedings, volume 1443 of Lecture Notes in Computer Science, pp.397-408, 1998.
DOI : 10.1007/BFb0055070

H. Goguen, A Typed Operational Semantics for Type Theory, 1994.
DOI : 10.1007/bfb0014053

H. Goguen, C. Mcbride, and J. Mckinna, Eliminating Dependent Pattern Matching, Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, 2006.
DOI : 10.1007/11780274_27

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.101.7522

G. Gonthier, The Four Colour Theorem: Engineering of a Formal Proof, Computer Mathematics, 8th Asian Symposium, p.333, 2007.
DOI : 10.1007/978-3-540-87827-8_28

B. Grégoire and J. L. Sacchini, On Strong Normalization of the Calculus of Constructions with Type-Based Termination, Logic for Programming, Artificial Intelligence, and Reasoning -17th International Conference, LPAR-17 Proceedings, pp.333-347, 2010.
DOI : 10.1007/978-3-642-16242-8_24

R. Harper, F. Honsell, and G. D. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

M. Hofmann and T. Streicher, The groupoid model refutes uniqueness of identity proofs, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.208-212, 1994.
DOI : 10.1109/LICS.1994.316071

J. Hughes, L. Pareto, and A. Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.410-423, 1996.
DOI : 10.1145/237721.240882

J. W. Klop, Combinatory Reduction Systems, 1980.

N. D. Chin-soon-lee, . Jones, M. Amir, and . Ben-amram, The size-change principle for program termination, POPL, pp.81-92, 2001.

G. Lee and B. Werner, A proof-irrelevant model of CIC with predicative induction and judgemental equality, 2010.

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4

URL : https://hal.archives-ouvertes.fr/inria-00360768

P. Letouzey, Programmation fonctionnelle certifiée ? L'extraction de programmes dans l'assistant Coq, 2004.

A. Levy, Basic Set Theory, 1979.
DOI : 10.1007/978-3-662-02308-2

Z. Luo, A higher-order calculus and theory abstraction, Information and Computation, vol.90, issue.1, pp.107-137, 1991.
DOI : 10.1016/0890-5401(91)90062-7

URL : http://doi.org/10.1016/0890-5401(91)90062-7

Z. Luo, Computation and reasoning: a type theory for computer science, 1994.

L. Magnusson and B. Nordström, The Alf proof editor and its proof engine, Barendregt and Nipkow, pp.213-237
DOI : 10.1007/3-540-58085-9_78

P. Martin-löf, An Intuitionistic Theory of Types: Predicative Part, Logic Colloquium '73, Proceedings of the Logic Colloquium of Studies in Logic and the Foundations of Mathematics, pp.73-118, 1975.
DOI : 10.1016/S0049-237X(08)71945-1

C. Mcbride, Dependently Typed Functional Programs and their Proofs, 1999.

C. Mcbride, Epigram: Practical Programming with Dependent Types, Estonia LNCS, vol.3622, 2004.
DOI : 10.1007/11546382_3

C. Mcbride, H. Goguen, and J. Mckinna, A Few Constructions on Constructors, Types for Proofs and Programs, pp.186-200, 2004.
DOI : 10.1007/11617990_12

C. Mcbride and J. Mckinna, The view from the left, Journal of Functional Programming, vol.14, issue.1, pp.69-111, 2004.
DOI : 10.1017/S0956796803004829

B. Paul-andrémellì-es and . Werner, A generic normalisation proof for pure type systems, Types for Proofs and Programs, International Workshop TYPES'96, pp.254-276, 1996.

N. Paul and M. , Inductive types and type constraints in the second-order lambda calculus, Ann. Pure Appl. Logic, vol.51, issue.12, pp.159-172, 1991.

A. Miquel, Le calcul des constructions implicite: syntaxe et sémantique, 2001.

A. Miquel and B. Werner, The Not So Simple Proof-Irrelevant Model of CC, Geuvers and Wiedijk [37], pp.240-258
DOI : 10.1007/3-540-39185-1_14

N. Mishra-linger and T. Sheard, Erasure and Polymorphism in Pure Type Systems, Amadio [9], pp.350-364
DOI : 10.1007/978-3-540-78499-9_25

B. Nordström, K. Petersson, and J. M. Smith, Programming in Martin-Löf 's Type Theory. An Introduction, 1990.

U. Norell, Towards a practical programming language based on dependent type theory, 2007.

N. Oury, Pattern matching coverage checking with dependent types using set approximations, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.47-56, 2007.
DOI : 10.1145/1292597.1292606

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.175.8980

L. Pareto, Types for Crash Prevention, 2000.

C. Paulin-mohring, Définitions Inductives en Théorie des Types d'Ordre Supérieur. HabilitationàHabilitationà diriger les recherches, 1996.

C. John and . Reynolds, Polymorphism is not set-theoretic, Semantics of Data Types, International Symposium Proceedings, pp.145-156, 1984.

T. Sheard and N. Linger, Programming in Omega, Central European Functional Programming School, Second Summer School Lecture Notes in Computer Science, vol.5161, pp.158-227, 2007.

V. Siles and H. Herbelin, Equality Is Typable in Semi-full Pure Type Systems, 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp.11-14, 2010.
DOI : 10.1109/LICS.2010.19

URL : https://hal.archives-ouvertes.fr/inria-00496988

V. Siles and H. Herbelin, Pure Type System conversion is always typable, Journal of Functional Programming, vol.1, issue.02, 2010.
DOI : 10.1017/S0956796805005770

URL : https://hal.archives-ouvertes.fr/inria-00497177

M. Sozeau, Subset Coercions in Coq, Types for Proofs and Programs, pp.237-252, 2006.
DOI : 10.1007/978-3-540-74464-1_16

URL : https://hal.archives-ouvertes.fr/inria-00628869

M. Sozeau, Equations: A Dependent Pattern-Matching Compiler, Interactive Theorem Proving, First International Conference Proceedings, pp.419-434, 2010.
DOI : 10.1007/978-3-642-14052-5_29

URL : https://hal.archives-ouvertes.fr/inria-00628862

A. Stump, M. Deters, A. Petcher, T. Schiller, and T. W. Simpson, Verified programming in Guru, Proceedings of the 3rd workshop on Programming languages meets program verification, PLPV '09, pp.49-58, 2009.
DOI : 10.1145/1481848.1481856

L. S. Van-benthem and . Jutting, Typing in pure type systems, Inf. Comput, vol.105, issue.1, pp.30-41, 1993.

D. Wahlstedt, Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion, 2007.

B. Werner, Sets in types, types in sets, Theoretical Aspects of Computer Software, Third International Symposium, TACS '97 Proceedings, volume 1281 of Lecture Notes in Computer Science, pp.530-346, 1997.
DOI : 10.1007/BFb0014566

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709

B. Werner, On the strength of proof-irrelevant type theories, Logical Methods in Computer Science, vol.4, issue.3, 2008.

H. Xi, Dependent Types for Program Termination Verification, Higher-Order and Symbolic Computation, vol.15, issue.1, pp.91-131, 2002.
DOI : 10.1023/A:1019916231463

H. Xi, Applied Type System (extended abstract), Post-Workshop Proceedings of TYPES 2003, pp.394-408, 2004.