Le lambda-calcul du second ordre

 Access to full text

 Full (PDF)

1. [1] J.Y. Girard : Une extension de l'interprétation de Gödel à l'analyse et son application à l'élimination des coupures dans l'analyse et la théorie des types, Proceedings Second Scandinavian Logic Symp. ed. Fenstad, pp. 63-92, North Holland, Amsterdam1971. Zbl0221.02013MR409133
2. [2] J.Y. Girard : Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, Thèse de Doctorat d'Etat, Université Paris VII,1972. 
3. [3] P. Martin Løf: Intuitionistic type theory, Bibliopolis, Napoli, 1984. Zbl0571.03030MR769301
4. [4] T. Coquand, G. Huet : A theory of constructions, Comptes-Rendus du Congrès de Logique d'Orsay, à paraître chez North-Holland. 
5. [5] J. Reynolds : Towards a theory of type structure, Lectures Notes in Computer Science19, pp. 408-423, Springer-Verlag1974. Zbl0309.68016MR458988
6. [6] J. Reynolds : Polymorphism is not set-theoretic, Lecture Notes in Computer Science173, pp. 145-156, Springer-Verlag1984. Zbl0554.03012MR784456
7. [7] D. Prawitz : Natural Deduction, Almqvitz & Wiksell, Stockholm, 1965. Zbl0173.00205MR193005
8. [8] W. Howard : The formulas-as-types notion of construction, in To H.B. Curry : Essays on Combinatory Logic, Lambda-Calculus and Formalism, ed. Seldin et Hindley, Academic Press1980. MR592816
9. [9] W. Tait : Intensional interpretation of functionals of finite types I, Journal of Symbolic Logic32 (1967), pp. 198-212. Zbl0174.01202MR219400
10. [10] J.L. Krivine : Un algorithme non typable dans le système F, note aux CHAS, 1987. Zbl0665.03008MR880113
11. [11] D. Scott : Domains for denotational semantics, Lecture Notes in Computer Science140, pp. 577-613, Springer-Verlag1982. Zbl0495.68025MR675486
12. [12] G. Berry : Modèles complètement adéquats et stables des lambda-calculs typés, Thèse de Doctorat d'Etat, Université Paris VII, 1979. 
13. [13] J.Y. Girard : The system F of variable types, fifteen years later, Theoretical Computer Science45 (1986), pp. 159-192. Zbl0623.03013MR867281
14. [14] J.Y. Girard : Linear Logic, à paraître dans Theoretical Computer Science. 
15. [15] J.Y. Girard, Y. Lafont : Linear Logic and lazy evaluation, à paraître dans les comptes-rendus du Congrès TAPTSOFT '87, Pisa. 
16. [16] J.Y. Girard : Multiplicatives, à paraître dans les comptes-rendus du Congrès tenu au I.S.I. de Torino, Octobre 1986. Zbl0667.03046
17. [17] J.L. Krivine : Une approche model-théorique à la programmation typée, en cours de rédaction. 

1. Philip J. Scott, Functorial polymorphism and semantic parametricity