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
Constructions, Inductive Types and Strong Normalization, 1993. ,
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
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
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
Foundations of constructive mathematics . Metamathematical studies, Ergebnisse der Mathematik und ihrer Grenzgebiete (3) [Results in Mathematics and Related Areas, 1985. ,
Abstract, The Journal of Symbolic Logic, vol.39, issue.02, pp.600-622, 1998. ,
DOI : 10.1007/BF02007566
Modified Bar Recursion and Classical Dependent Choice. Logic Colloquium '01, Lect. Notes Log. Assoc. Symbol. Logic, vol.20, pp.89-107, 2005. ,
Continuous semantics for strong normalisation, Mathematical Structures in Computer Science, vol.16, issue.05, pp.23-34, 2005. ,
DOI : 10.1017/S0960129506005457
A Computational Interpretation of Open Induction. Proceeding of LICS, 2004. ,
Continuous Functionals of Dependent and Transfinite Types, Models and Computability, pp.1-22, 1999. ,
DOI : 10.1017/CBO9780511565670.002
A Logical Framework with Dependently Typed Record, Fundam. Inform, vol.65, issue.1-2, pp.113-134, 2005. ,
A proof-irrelevant model of Martin-Lf's logical framework, Math. Structures Comput. Sci, vol.12, issue.6, pp.771-795, 2002. ,
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
Lecture note on the domain interpretation of type theory, Workshop on Semantics of Programming Languages, 1983. ,
Martin-Löf Type Theory. Handbook of Logic in Computer Science, 2000. ,
Closure under alpha-conversion, Lecture Notes in Computer Science, vol.806, pp.313-332, 1993. ,
DOI : 10.1007/3-540-58085-9_82
A type assignment for the strongly normalizable terms, To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, pp.561-577, 1980. ,
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
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. ,
Combinators and classes, Lecture Notes in Comput. Sci, vol.37, pp.1-26, 1975. ,
DOI : 10.1007/BFb0029517
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
Semantics of Type Theory. in the series Progress in Theoretical Computer Science, Basel: Birkhaeuser. XII, 1991. ,
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