@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://www.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://www.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://www.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, in Séminaire Bourbaki : volume 1986/87, exposés 669-685, Astérisque, no. 152-153 (1987), Talk no. 678, 13 p. http://www.numdam.org/item/SB_1986-1987__29__173_0/
[1] 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] 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] : Intuitionistic type theory, Bibliopolis, Napoli, 1984. | MR | Zbl
[4] A theory of constructions, Comptes-Rendus du Congrès de Logique d'Orsay, à paraître chez North-Holland.
, :[5] Towards a theory of type structure, Lectures Notes in Computer Science 19, pp. 408-423, Springer-Verlag 1974. | MR | Zbl
:[6] Polymorphism is not set-theoretic, Lecture Notes in Computer Science 173, pp. 145-156, Springer-Verlag 1984. | MR | Zbl
:[7] Natural Deduction, Almqvitz & Wiksell, Stockholm, 1965. | MR | Zbl
:[8] 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] Intensional interpretation of functionals of finite types I, Journal of Symbolic Logic 32 (1967), pp. 198-212. | MR | Zbl
:[10] Un algorithme non typable dans le système F, note aux CHAS, 1987. | MR | Zbl
:[11] Domains for denotational semantics, Lecture Notes in Computer Science 140, pp. 577-613, Springer-Verlag 1982. | MR | Zbl
:[12] Modèles complètement adéquats et stables des lambda-calculs typés, Thèse de Doctorat d'Etat, Université Paris VII, 1979.
:[13] The system F of variable types, fifteen years later, Theoretical Computer Science 45 (1986), pp. 159-192. | MR | Zbl
:[14] Linear Logic, à paraître dans Theoretical Computer Science.
:[15] Linear Logic and lazy evaluation, à paraître dans les comptes-rendus du Congrès TAPTSOFT '87, Pisa.
, :[16] Multiplicatives, à paraître dans les comptes-rendus du Congrès tenu au I.S.I. de Torino, Octobre 1986. | Zbl
:[17] Une approche model-théorique à la programmation typée, en cours de rédaction.
: