P. Aczel, Frege Structures and the Notions of Proposition, Truth and Set, Stud. Logic Foundations Math, vol.101, pp.31-59, 1980.
DOI : 10.1016/S0049-237X(08)71252-7

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

R. Amadio and P. L. Curien, Domains and Lambda-Calculi. Cambridge tracts in theoretical computer science, p.46, 1997.
DOI : 10.1017/cbo9780511983504

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

S. Van-bakel, Complete restrictions of the intersection type discipline, Theoretical Computer Science, vol.102, issue.1, pp.135-163, 1992.
DOI : 10.1016/0304-3975(92)90297-S

H. Barendregt, M. Coppo, and M. Dezani-ciancaglini, A filter lambda model and the completeness of type assignment, The Journal of Symbolic Logic, vol.37, issue.04, pp.931-940, 1983.
DOI : 10.1002/malq.19800261902

M. Beeson, Foundations of constructive mathematics . Metamathematical studies, Ergebnisse der Mathematik und ihrer Grenzgebiete (3) [Results in Mathematics and Related Areas, 1985.

S. Berardi, M. Bezem, . Th, and . Coquand, Abstract, The Journal of Symbolic Logic, vol.39, issue.02, pp.600-622, 1998.
DOI : 10.1007/BF02007566

U. Berger and P. Oliva, Modified Bar Recursion and Classical Dependent Choice. Logic Colloquium '01, Lect. Notes Log. Assoc. Symbol. Logic, vol.20, pp.89-107, 2005.

U. Berger, Continuous semantics for strong normalisation, Mathematical Structures in Computer Science, vol.16, issue.05, pp.23-34, 2005.
DOI : 10.1017/S0960129506005457

U. Berger, A Computational Interpretation of Open Induction. Proceeding of LICS, 2004.

U. Berger, Continuous Functionals of Dependent and Transfinite Types, Models and Computability, pp.1-22, 1999.
DOI : 10.1017/CBO9780511565670.002

. Th, R. Coquand, M. Pollack, and . Takeyama, A Logical Framework with Dependently Typed Record, Fundam. Inform, vol.65, issue.1-2, pp.113-134, 2005.

D. Fridlender, A proof-irrelevant model of Martin-Lf's logical framework, Math. Structures Comput. Sci, vol.12, issue.6, pp.771-795, 2002.

R. Harper and F. Pfenning, On equivalence and canonical forms in the LF type theory, ACM Transactions on Computational Logic, vol.6, issue.1, pp.61-101, 2005.
DOI : 10.1145/1042038.1042041

P. Martin-löf, Lecture note on the domain interpretation of type theory, Workshop on Semantics of Programming Languages, 1983.

B. Nordstrom, J. Petersson, and . Smith, Martin-Löf Type Theory. Handbook of Logic in Computer Science, 2000.

]. R. Pollack, Closure under alpha-conversion, Lecture Notes in Computer Science, vol.806, pp.313-332, 1993.
DOI : 10.1007/3-540-58085-9_82

G. Pottinger, A type assignment for the strongly normalizable terms, To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, pp.561-577, 1980.

G. Plotkin, LCF considered as a programming language, Theoretical Computer Science, vol.5, issue.3, pp.223-255, 1977.
DOI : 10.1016/0304-3975(77)90044-5

D. Scott, Lectures on a mathematical theory of computation. Theoretical foundations of programming methodology, NATO Adv. Study Inst. Ser. C: Math. Phys. Sci, vol.91, pp.145-292, 1981.

D. Scott, Combinators and classes, Lecture Notes in Comput. Sci, vol.37, pp.1-26, 1975.
DOI : 10.1007/BFb0029517

C. Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, 1962.
DOI : 10.1090/pspum/005/0154801

. Th and . Streicher, Semantics of Type Theory. in the series Progress in Theoretical Computer Science, Basel: Birkhaeuser. XII, 1991.

W. W. Tait, Normal Form Theorem for Bar Recursive Functions of Finite Type, Proceedings of the Second Scandinavian Logic Symposium, 1971.
DOI : 10.1016/S0049-237X(08)70853-X