Le lambda-calcul du second ordre
Séminaire Bourbaki : volume 1986/87, exposés 669-685, Astérisque no. 152-153  (1987), Talk no. 678, p. 173-185
@incollection{SB_1986-1987__29__173_0,
     author = {Girard, Jean-Yves},
     title = {Le lambda-calcul du second ordre},
     booktitle = {S\'eminaire Bourbaki : volume 1986/87, expos\'es 669-685},
     author = {Collectif},
     series = {Ast\'erisque},
     publisher = {Soci\'et\'e math\'ematique de France},
     number = {152-153},
     year = {1987},
     note = {talk:678},
     pages = {173-185},
     zbl = {0645.03013},
     mrnumber = {936854},
     language = {fr},
     url = {http://www.numdam.org/item/SB_1986-1987__29__173_0}
}
Girard, Jean-Yves. Le lambda-calcul du second ordre, in Séminaire Bourbaki : volume 1986/87, exposés 669-685, Astérisque, no. 152-153 (1987), Talk no. 678, pp. 173-185. http://www.numdam.org/item/SB_1986-1987__29__173_0/

[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, Amsterdam 1971. | MR 409133 | Zbl 0221.02013

[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] P. Martin Løf : Intuitionistic type theory, Bibliopolis, Napoli, 1984. | MR 769301 | Zbl 0571.03030

[4] T. Coquand, G. Huet : A theory of constructions, Comptes-Rendus du Congrès de Logique d'Orsay, à paraître chez North-Holland.

[5] J. Reynolds : Towards a theory of type structure, Lectures Notes in Computer Science 19, pp. 408-423, Springer-Verlag 1974. | MR 458988 | Zbl 0309.68016

[6] J. Reynolds : Polymorphism is not set-theoretic, Lecture Notes in Computer Science 173, pp. 145-156, Springer-Verlag 1984. | MR 784456 | Zbl 0554.03012

[7] D. Prawitz : Natural Deduction, Almqvitz & Wiksell, Stockholm, 1965. | MR 193005 | Zbl 0173.00205

[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 Press 1980. | MR 592816

[9] W. Tait : Intensional interpretation of functionals of finite types I, Journal of Symbolic Logic 32 (1967), pp. 198-212. | MR 219400 | Zbl 0174.01202

[10] J. L. Krivine : Un algorithme non typable dans le système F, note aux CHAS, 1987. | MR 880113 | Zbl 0665.03008

[11] D. Scott : Domains for denotational semantics, Lecture Notes in Computer Science 140, pp. 577-613, Springer-Verlag 1982. | MR 675486 | Zbl 0495.68025

[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] J. Y. Girard : The system F of variable types, fifteen years later, Theoretical Computer Science 45 (1986), pp. 159-192. | MR 867281 | Zbl 0623.03013

[14] J. Y. Girard : Linear Logic, à paraître dans Theoretical Computer Science.

[15] J. Y. Girard, Y. Lafont : Linear Logic and lazy evaluation, à paraître dans les comptes-rendus du Congrès TAPTSOFT '87, Pisa.

[16] J. Y. Girard : Multiplicatives, à paraître dans les comptes-rendus du Congrès tenu au I.S.I. de Torino, Octobre 1986. | Zbl 0667.03046

[17] J. L. Krivine : Une approche model-théorique à la programmation typée, en cours de rédaction.