Le lambda-calcul du second ordre
Séminaire Bourbaki : volume 1986/87, exposés 669-685, Astérisque, no. 152-153 (1987), Exposé no. 678, 13 p. 
@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},
     series = {Ast\'erisque},
     note = {talk:678},
     pages = {173--185},
     publisher = {Soci\'et\'e math\'ematique de France},
     number = {152-153},
     year = {1987},
     mrnumber = {936854},
     zbl = {0645.03013},
     language = {fr},
     url = {http://archive.numdam.org/item/SB_1986-1987__29__173_0/}
}
TY  - CHAP
AU  - Girard, Jean-Yves
TI  - Le lambda-calcul du second ordre
BT  - Séminaire Bourbaki : volume 1986/87, exposés 669-685
AU  - Collectif
T3  - Astérisque
N1  - talk:678
PY  - 1987
SP  - 173
EP  - 185
IS  - 152-153
PB  - Société mathématique de France
UR  - http://archive.numdam.org/item/SB_1986-1987__29__173_0/
LA  - fr
ID  - SB_1986-1987__29__173_0
ER  - 
%0 Book Section
%A Girard, Jean-Yves
%T Le lambda-calcul du second ordre
%B Séminaire Bourbaki : volume 1986/87, exposés 669-685
%A Collectif
%S Astérisque
%Z talk:678
%D 1987
%P 173-185
%N 152-153
%I Société mathématique de France
%U http://archive.numdam.org/item/SB_1986-1987__29__173_0/
%G fr
%F SB_1986-1987__29__173_0
Girard, Jean-Yves. Le lambda-calcul du second ordre, dans Séminaire Bourbaki : volume 1986/87, exposés 669-685, Astérisque, no. 152-153 (1987), Exposé no. 678, 13 p. http://archive.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 | Zbl

[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 | Zbl

[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 | Zbl

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

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

[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

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

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

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

[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 | Zbl

[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

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