?. ?. If and A. ?x, B : T then there are s 1 , s 2 , s 3 such that (s 1 , s 2 , s 3 ) ? R, ? ? e A : s 1 , ?(x : A) ? e B : s 2

?. ?. If, ?. ?. , and A. , M : T then there are s 1 , s 2 , s 3 and B such that (s 1 , s 2 , s 3 )

A. Abel, Towards Normalization by Evaluation for the ? ?-Calculus of Constructions. Pages 224?239 of, Functional and Logic Programming, 10th International Symposium, FLOPS 2010, 2010.

A. Abel, T. Coquand, and P. Dybjer, Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements, Pages 3?12 of: 22nd IEEE Symposium on Logic in Computer Science, pp.10-12, 2007.

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

H. Barendregt, Introduction to Generalized Type Systems, Journal of Functional Programming, vol.1, issue.2, pp.125-154, 1991.

H. P. Barendregt, Lambda Calculi with Types. Pages 117?309 of, Handbook of Logic in Computer Science, 1992.

S. Berardi, Type Dependence and Constructive Mathematics, 1990.

N. G. De-bruijn, Lambda-Calculus Notation with Nameless Dummies: a Tool for Automatic Formula Manipulation with Application to the Church-Rosser Theorem, Indagtiones Mathematica, vol.34, issue.5, pp.381-392, 1972.

H. Geuvers, Logics and Type Systems, 1993.

H. Geuvers and M. Nederhof, Modular Proof of Strong Normalization for the Calculus of Constructions, Journal of Functional Programming, vol.1, issue.2, pp.155-189, 1991.

H. Geuvers and B. Werner, On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, 1994.
DOI : 10.1109/LICS.1994.316057

H. Goguen, A Typed Operational Semantics for Type Theory, 1994.

Z. Luo, ECC: an Extended Calculus of Constructions. Pages 385?395 of, Proceedings of the Fourth Annual Symposium on Logic in Computer Science, 1989.

P. Martin-löf, P. Werner, and B. , Intuitionistic Type Theory A Generic Normalization Proof for Pure Type Systems, TYPES'96, 1984.

B. Nordstrom, 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, pp.412-96, 2007.

R. Pollack, The theory of LEGO: A proof checker for the extended calculus of constructions, 1994.

V. Siles, Formalization of Equivalence between PTS and PTSe, 2010.

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

T. Streicher, Semantics of Type Theory: Correctness, Completeness, and Independence Results, 1991.
DOI : 10.1007/978-1-4612-0433-6

J. Terlouw, Een nadere bewijstheoretische analyse van GSTTs (Manuscript, in Dutch), Typing in Pure Type Systems. Information and Computation, pp.30-41, 1989.

L. S. Van-benthem-jutting, J. Mckinna, and R. Pollack, Checking algorithms for Pure Type Systems, 1993.
DOI : 10.1007/3-540-58085-9_71

B. Werner, Une théorie des Constructions Inductives, 1994.

B. Werner and G. Lee, A Proof-Irrelevant Model of CIC with Predicate Induction and Judgemental Equality, 2010.