C. La-relation and ?. De-synthèse-de-type, Étant donnés ? et t, cette relation essaye de générer une contrainte C et de synthétiser un type T tels que C

C. La-relation and ?. De-vérification-de-type, Étant donnés ? , t et T , cette relation essayer de générer une contrainte C telle que C

. Ainsi and . De-même-que-dans, ces relations de synthèse et de vérification de type mélangent deux paradigmes de l'inférence/vérification de type : ? L'inférence/vérification de type bi-directionnelle, voir par exemple [DP00, Abe04], dans laquelle sont utilisées une relation d'inférence de type et une relation de vérification de types. Le processus d'inférence

(. Tu, D'après l'hypothèse d'induction et le lemme 11.3.16 on a

(. ×i, D'après l'hypothèse d'induction et le lemme 11.3.16 on a C 1 ? C 2 ; ? ? t i : T i pour tout i ? {1, 2}, d'où C 1 ? C 2

E. (. Posons and C. Def, D'après l'hypothèse d'induction et le lemme 11.3.16, on a E; ? ? t : ? ?P.T et E ? P; ?, x : T ? u : U. Il s'en suit que, 'autre part, on a ? E ? ? ?P et ? / ? FV(E, ?, ? ?P.U) car ? / ? FV(C, ? )

E. (. Posons and . Def-?-?p??-?-(-p-?-c-), Par l'hypothèse d'induction et le lemme 11, ) car ? / ? FV(? )

E. (. Posons and C. Def, D'après l'hypothèse d'induction et le lemme 11.3.16, on a E; ? ? t : ? ?P.T , d'où E; ? ? t

E. (. Posons, C. ?. Def, ?. , and U. , D'après l'hypothèse d'induction et le lemme 11

. Sub, Par hypothèse d'induction et en

. On-aborde-maintenant-le-cas-des-constructeurs-c-?-c-{1, Afin de produire les bonnes interactions, on utilise des éliminateurs pour les constructeurs. À chaque constructeur c ? C avec a c > 0, on associe des symboles d'arité nulle d c,1 , . . . , d c,ac appelés destructeurs

T. Comme and . ??×, on a T µ ? CR CR par le lemme 11.4.18, donc comme ite(c, u 1 , u 2 ) est neutre, il suffit de montrer que (ite(c, u 1 , u 2 )) SR ? T µ, ) avec (c, u 1 , u 2 ) ? SR (c ?

?. Sinon and . Et-v-=-u-i-?-t-?-par-hypothèse, (let) Soit (µ, ?) | = C; ? . On doit montrer que (let x = t in u)? ? Uµ. Par le lemme 1.2.10, on peut supposer que x / ? FV(?) ? Dom(?) On a donc

(. Soit, On doit montrer que t? ? T µ[ a/ ?] pour tout a tel que µ

(. Soit, |. P. Comme-?, |. , and ?. , Par hypothèse d'induction, t? ? T µ[ a/ ?] pour tout a tel que µ

(. Comme-?, |. , and ?. , Par hypothèse d'induction, on a t? ? T

(. Soit, On doit montrer que (let x = t in u)?. En raisonnant comme dans le cas de la règle (let), on peut supposer que x / ? FV(?) ? Dom(?) et il

?. P. Du-fait-que-?-|-=-c-et-que-?-c-?-?-? and . Tel-que-?, Il s'en suit que t? ? T µ

C. Si, T et s'il existe un assignement µ tel que µ | = C

A. , R. M. Abramsky, D. Gabbay, and T. Maibaum, Termination Checking with Types Special Issue (FICS'03) 160 Amadio et P.-L. Curien ? Domains and Lambda-Calculi, Cambridge Tracts in Theoretical Computer Science Avenhaus et C. Loría-Sáenz ? « Higher Order Conditional Rewriting and Narrowing Barendregt ? The Lambda-Calculus, its Syntax and Semantics, Studies in Logic and the Foundation of Mathematics, Bibliographie [Abe03] A. Abel ? « Termination and Productivity Checking with Continuous Types Proceedings of TLCA'03 Semi-Continuous Sized Types and Termination Proceedings of CSL'06 Proceedings of the 1st International Conference on Constraints in Computational LogicsAlt93] T. Altenkirch ? « Constructions, Inductive Types and Strong Normalization Thèse Lambda Calculi with Types », Handbook of Logic in Computer Science Bezem et T. Coquand ? « On the Computational Content of the Axiom of ChoiceBBF96] S. van Bakel, F. Barbanera et M. Fernández ? « Rewrite Systems with Abstraction and ?-rule : Types, Approximants and Normalisation Proceedings of ESOP'96, pp.1-15, 1984.

F. Barbanera and M. , Dezani-Ciancaglini et U. de' Liguoro ? « Intersection and Union Types : Syntax and Semantics, pp.202-230, 1995.

M. [. Barbanera and . Fernández, Modularity of strong normalization in the algebraic-??-cube, Journal of Functional Programming, vol.7, issue.6, pp.613-660, 0198.
DOI : 10.1017/S095679689700289X

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

B. [. Barthe, Grégoire et F. Pastawski ? « Practical Inference ofr Type-Based Termination in a Polymorphic Setting, Proceedings of TL- CA'05, pp.71-85, 2005.

«. [. Type, F. Blanqui, and J. , Based Termination of Recursives Definitions in the Calculus of Inductive Constructions, Proceedings of LPAR'06 Jouannaud et M. Okada ? « Inductive-Data-Types Systems, pp.257-271, 2002.

J. [. Blanqui, Jouannaud et A. Rubio ? « HORPO with Computability Closure : A Reconstruction, Proceedings of LPAR'07, pp.138-150, 2007.

B. , J. A. Bergstra, and J. W. , Klop ? « Conditional rewrite rules : Confluence and termination », Journal of Computer and System Sciences, vol.32, issue.3, pp.323-362, 1986.
DOI : 10.1016/0022-0000(86)90033-4

URL : https://doi.org/10.1016/0022-0000(86)90033-4

E. Bonelli and D. , de Bruijn Indices for Metaterms, Journal of Logic and Computation, vol.15, issue.6, pp.855-899, 2005.
DOI : 10.1093/logcom/exi051

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

C. [. Blanqui and C. Kirchner, Riba ? « On the Confluence of Lambda- Calculus with Conditional Rewriting, Proceedings of FoSSaCS'06, pp.17-130, 2006.

M. Coppo, A new type assignment for ??-terms, Archiv f??r Mathematische Logik und Grundlagenforschung, vol.5, issue.1, pp.139-156, 1978.
DOI : 10.1007/BF02011875

J. [. Comon, ?. Jouannaud, and . Termes-en-logique-et-en-programmation, Notes de cours de DEA, 13 [CP88] T. Coquand et C. Paulin ? « Inductively defined types », Conference on Computer Logic Proceedings of LiCS'06 ? « Combining First Order Algebraic Rewriting Systems, Recursion and Extensional Lambda Calculi Proceedings of ICALP Combining First Order Algebraic Rewriting Systems, Recursion and Extensional Lambda Calculi, pp.30-50, 1988.

M. Dezani-ciancaglini, U. De-'liguoro, and P. , Filter models for conjunctive-disjunctive ??-calculi, Theoretical Computer Science, vol.170, issue.1-2, pp.83-128, 1996.
DOI : 10.1016/S0304-3975(96)80703-1

URL : http://www.di.unito.it/~dezani/papers/8.ps.gz

?. , «. Filter, C. Model, and . Lambda-calculus, Kirchner ? « Higher Order Unification via Explicit Substitutions Handbook of Theoretical Computer Science, Volume B : Formal Models and Sematics (B) (J. van Leeuwen, Siam Journal on Computing Theorem Proving ModuloDJ90] N. Dershowitz et J.-P. Jouannaud ? « Rewrite Systems Proceedings of CSL'00DO90] N. Dershowitz et M. Okada ? « A rationale for conditional equational programming « Adding Algebraic Rewriting to the Untyped Lambda CalculusDow06] G Dowek ? « Truth Values Algebras and Proof Normalization », Post Proceedings of TYPES'06 Davis et F. Pfenning ? « Intersection Types and Computational Effects Proceedings of ICFP'00 Fisher et M. O. Rabin ? « Super-Exponential Complexity of Presburger Arithmetic », Proceedings on the SIAM-AMS Symposium in Applied Mathematics, pp.1376-1419, 1974.

]. J. Gal89, Gallier ? « On Girard's " Candidats de Reducibilité " », Logic and Computer Science (P. Odifredi, éd, pp.74-164, 1989.

]. ?. Gal91 and «. What, s So Special About Kruskal's Theorem and the Ordinal ? 0 ? A Survey of Some Results in Proof Theory, Annals of Pure and Applied Logic, vol.53, issue.22, pp.199-260, 0190.

G. J. Glauert and D. Kesner, Khasidashvili ? « Expression Reduction Systems and Extensions : An Overview, Processes, Terms and Cycles : Steps to the Road of Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion os His 60th Birthday, pp.496-553, 2005.

G. Girard and Y. , Lafont et P. Taylor ? Proofs and Types, Cambridge Tracts in Theoretical Computer Science, Giovannetti et C. Moiso ? « Notes on the Elimination of Conditions Proceedings of CTRS'87, pp.188-91, 1988.

J. [. Harper, ?. Mitchell, . Parametricity, . Variants, J. Girard-'s et al., Parametricity and variants of Girard's operator, HPS96] J. Hughes, L. Pareto et A. Sabry ? « Proving the Correctness of Reactive Systems Using Sized Types Proceedings of POPL'96, pp.1-5, 1996.
DOI : 10.1016/S0020-0190(99)00036-8

[. Jouannaud, Kirchner ? « Completion of a Set of Rules Modulo a Set of Equations, Siam Journal on Computing, vol.25, issue.4, pp.1155-1194, 1986.

[. Jim, Full Abstraction and the Context Lemma, Jouannaud et M. Okada ? « Executable Higher-Order Algebraic Specification Languages Proceedings of LiCS'91, pp.663-696, 1991.
DOI : 10.1137/S0097539791224212

[. Jouannaud, Abstract data type systems, Proceedings of RTA'06 Jouannaud et A. Rubio ? « The Higher-Order Recursive Path Ordering Proceedings of LiCS'99, pp.349-391, 1997.
DOI : 10.1016/S0304-3975(96)00161-2

R. Kennaway, J. W. Klop, R. Sleep, and F. , Comparing Curried and Uncurried Rewriting, de Vries ? « Comparing Curried and Uncurried Rewriting, pp.15-39, 0199.
DOI : 10.1006/jsco.1996.0002

J. W. Klop, A. Middeldorp, Y. Toyama, and R. C. , Modularity of confluence: A simplified proof, de Vrijer ? « Modularity of Confluence : A Simplified Proof Klop, V. van Oostrom et F. van Raamsdonk ? « Combinatory Reduction Systems : Introduction and Survey, pp.101-109, 1993.
DOI : 10.1016/0020-0190(94)90034-5

]. X. Ldg-+-07, D. Leroy, J. Doligez, D. Garrique, and . Rémy, Vouillon ? The Objective Caml System Release 3, 13 [Luo90] Z. Luo ? « An Extended Calculus of Constructions Thèse, p.160, 1990.

«. Mat05-]-? and . Non, Strictly Positive Fixed-Points for Classical Natural Deduction, Proceedings of LiCS'98Men87] N. P. Menler ? « Recursive Types and Type Constraints in Second Ordel Lambda-Calculus Proceedings of LiCS'87, pp.205-230, 1987.

D. Miller, G. Nadathur, and F. , Pfenning et A. Scedrov ? « Uniform Proofs as a Foundation for Logic Programming, Annals of Pure and Applied Logic, vol.52, issue.12, pp.125-157, 1991.

G. [. Macqueen, An ideal model for recursive polymorphic types, Information and Control, vol.71, issue.1-2, pp.95-130, 1986.
DOI : 10.1016/S0019-9958(86)80019-5

R. Milner, M. Tofte, R. Harper, and D. , MacQueen ? The Defintion of Standard ML, p.13, 1997.

[. Melliès, Vouillon ? « Recursive Polymorphic Types and Parametricity in an Operational Framework, Proceedings of LiCS'05, pp.82-91, 2005.

?. Terese and . Systems, Cambridge Tracts in Theoretical Computer Science, pp.51-58, 2003.