, Frederic Gilbert Extending higher-order logic with predicate subtyping: application to PVS, 2018.

A. Abel and G. Scherer, On irrelevance and algorithmic equality in predicative type theory, 2012.

H. Barendregt, Introduction to generalized type systems, Journal of functional programming, vol.1, issue.2, pp.125-154, 1991.

H. Barendregt, Lambda calculi with types, handbook of logic in computer science vol, vol.ii, 1992.

B. Barras, S. Boutin, C. Cornes, J. Courant, J. Filliatre et al., The Coq proof assistant reference manual: Version 6.1. PhD thesis, Inria, 1997.
URL : https://hal.archives-ouvertes.fr/inria-00069968

G. Barthe, Type-checking injective pure type systems, Journal of Functional Programming, vol.9, issue.06, pp.675-698, 1999.

S. Berardi, Towards a mathematical analysis of the coquand-huet calculus of constructions and the other systems in barendregts cube, 1988.

B. Bernardo, An implicit Calculus of Constructions with dependent sums and decidable type inference, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01197380

K. Futatsugi, J. Joseph-a-goguen, J. Jouannaud, and . Meseguer, Principles of obj2, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp.52-66, 1985.

H. Geuvers, A short and flexible proof of strong normalization for the calculus of constructions, International Workshop on Types for Proofs and Programs, pp.14-38, 1994.

H. Geuvers and M. Nederhof, Modular proof of strong normalization for the calculus of constructions, Journal of Functional Programming, vol.1, issue.02, pp.155-189, 1991.

J. Girard, Interprétation fonctionelle etéliminationetélimination des coupures de larithmétique dordre supérieur, 1972.

M. Andrew, D. Kent, S. Kempe, and . Tobin-hochstadt, Occurrence typing modulo theories, ACM SIGPLAN Notices, vol.51, pp.296-309, 2016.

J. W. Klop, V. Van-oostrom, and F. Van-raamsdonk, Combinatory reduction systems: introduction and survey, Theoretical Computer Science, vol.121, issue.1, pp.279-308, 1993.

K. Knowles and C. Flanagan, Hybrid type checking, ACM Transactions on Programming Languages and Systems, vol.32, issue.TOPLAS, p.6, 2010.

Z. Luo, Ecc, an extended calculus of constructions, Logic in Computer Science, 1989. LICS'89, Proceedings., Fourth Annual Symposium on, pp.386-395, 1989.

S. Owre, N. John-m-rushby, and . Shankar, Pvs: A prototype verification system, International Conference on Automated Deduction, pp.748-752, 1992.

S. Owre and N. Shankar, The formal semantics of pvs, 1999.

M. Patrick-m-rondon, R. Kawaguci, and . Jhala, Liquid types, ACM SIGPLAN Notices, vol.43, pp.159-169, 2008.

J. Rushby, S. Owre, and N. Shankar, Subtypes for specifications: Predicate subtyping in pvs, IEEE Transactions on Software Engineering, vol.24, issue.9, pp.709-720, 1998.

V. Siles and H. Herbelin, Pure type system conversion is always typable, Journal of Functional Programming, vol.22, issue.2, pp.153-180, 2012.
URL : https://hal.archives-ouvertes.fr/inria-00497177

M. Sozeau, Subset coercions in coq, International Workshop on Types for Proofs and Programs, pp.237-252, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00628869

W. William and . Tait, A realizability interpretation of the theory of species, Logic Colloquium, pp.240-251, 1975.

J. Terlouw, Een nadere bewijstheoretische analyse van gstts, 1989.

J. Terlouw, Sterke normaliszatie in c a la tait, Notes of atalk held at the Intercity Seminar on Typed Lambda Calculus, 1989.

J. Terlouw, Strong normalization in type systems: A model theoretical approach, Annals of Pure and Applied Logic, vol.73, issue.1, pp.53-78, 1995.

B. Werner, This final step uses in turn termination in order to ensure the success of the expected algorithms. The proof of these three successive steps involves no further specific difficulty. Last, complete algorithms of type-checking and type inference are defined as follows, which states that whenever ? M : T is derivable (resp. ? T : s and ? M : T are derivable), then Infer-type-aux(? | M ) outputs some term successfully (resp. Check-type-aux(? | M | T ) succeeds), vol.4130, pp.604-618, 2006.

, Check-wf(? ) is defined as follows: if ? = ?, terminate successfully. Else, ? has the form ? , v : T. If v ? DV (? ) and Check-wf(? ) succeeds, continue as follows: if Infer-type-aux(? | T ) returns s(v) successfully, terminate successfully, all other cases, fail. Infer-type(? | M ) is defined as follows: if Check-wf(? ) succeeds, return Infer-type-aux(? | M ), else fail. Check-type(? | M | T ) is defined as follows: if Check-wf(? ) succeeds, continue as follows. If T = Kind and Infer-type-aux(? | M ) returns Kind, terminate successfully. If T = Kind and Infer-type-aux(? | T ) returns some

, The specifications expected from these algorithms are the following

, Theorem 13. The algorithms Check-wf, Infer-type, and Check-type always terminate, and admit the following properties:-Check-wf(? ) succeeds if and only if ? W F is derivable-Infer-type(? | M ) succeeds if only if there exists a term T such that ? M : T is derivable, in which case it outputs such a term-Check-type(? | M | T ) succeeds if only if ? M : T is derivable