Lambda Calculi with Types, Handbook of Logic in Computer Science, 1991. ,
Introduction to Generalised Type Systems, Journal of Functional Programming, vol.1, issue.2, pp.125-154, 1991. ,
Towards a Mathematical Analysis of Type Dependence in Coquand?Huet Calculus of Constructions and the Other Systems in Barendregt's Cube, 1988. ,
Modified Basic Functionality in Combinatory Logic, Dialectica, 1969. ,
Metamathematical Investigations of a Calculus of Constructions, Logic and Computer Science, pp.91-122, 1990. ,
The Calculus of Constructions, Information and Computation, pp.95-120, 1988. ,
The undecidability of typability in the Lambda-Pi-calculus, Proc. Typed Lambda Calculi and Applications, pp.139-145, 1993. ,
DOI : 10.1007/BFb0037103
Modular Proof of Strong Normalization for the Calculus of Constructions, Journal of Functional Programming, vol.1, issue.2, pp.155-189, 1991. ,
Characterization of typings in polymorphic type discipline, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.61-70, 1988. ,
DOI : 10.1109/LICS.1988.5101
Type Inference: Some Results, Some Problems, Fundamenta Informaticae, vol.19, issue.12, pp.87-126, 1993. ,
The system F of variable types, fifteen years later, Theoretical Computer Science, vol.45, pp.159-192, 1987. ,
DOI : 10.1016/0304-3975(86)90044-7
A framework for defining logics, Journal of the ACM, vol.40, issue.1, 1993. ,
DOI : 10.1145/138027.138060
Combinatory Reduction Systems, 1980. ,
Polymorphic type inference, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '83, pp.88-98, 1983. ,
DOI : 10.1145/567067.567077
Towards a theory of type structure, Proc. Paris Colloquium on Programming, pp.408-425, 1974. ,
DOI : 10.1007/3-540-06859-7_148