Light linear logic,
Logic and computational complexity (Indianapolis, IN, 1994), 145--176, Lecture Notes in Comput. Sci., 960, Springer, Berlin, 1995 and also in Information and Computation 143, no. 2, 175--204, 1998
[Gir98b]
Linear logic 96,
Papers from the meeting held at Keio University, Tokyo, March 28--April 2, 1996. Edited by Jean-Yves Girard, Mitsuhiro Okada and Andre Scedrov. Electronic Notes in Theoretical Computer Science, 3. Elsevier Science B.V., Amsterdam, 310 pp. (electronic), 1996
Proof-nets: the parallel syntax for proof-theory,
Logic and algebra (Pontignano, 1994), 97--124, Lecture Notes in Pure and Appl. Math., 180, Dekker, New York, 1996
Geometry of interaction. III. Accommodating the additives,
Advances in linear logic (Ithaca, NY, 1993), 329--389, London Math. Soc. Lecture Note Ser., 222, Cambridge Univ. Press, Cambridge, 1995
On geometry of interaction,
Proof and computation (Marktoberdorf, 1993), 145--191, NATO Adv. Sci. Inst. Ser. F Comput. Systems Sci., 139, Springer, Berlin, 1995
Linear logic: its syntax and semantics,
Advances in linear logic (Ithaca, NY, 1993), 1--42, London Math. Soc. Lecture Note Ser., 222, Cambridge Univ. Press, Cambridge, 1995
Advances in linear logic,
Proceedings of the workshop held at Cornell University, Ithaca, New York, June 14--18, 1993. Edited by Jean-Yves Girard, Yves Lafont and Laurent Regnier. London Mathematical Society Lecture Note Series, 222. Cambridge University Press, Cambridge, 1995
La logique au milieu du gué : logique naturelle et intelligence artificielle,
La machine de Turing, Le Seuil, Paris, 1995
Linear logic: a survey,
Logic and algebra of specification (Marktoberdorf, 1991), 63--112, NATO Adv. Sci. Inst. Ser. F Comput. Systems Sci., 94, Springer, Berlin, 1993 and also in The Curry-Howard isomorphism, 193--255, Cahiers Centre Logique, 8, Academia, Louvain-la-Neuve, 1995
Théorie réductrice de la démonstration,
Enciclopedia Italiana, Storia del 20° secolo, Roma, 1994
On the unity of logic,
Fourth Asian Logic Conference (Tokyo, 1990). Ann. Pure Appl. Logic 59, no. 3, 201--217, 1993
Embeddability of ptykes,
J. Symbolic Logic 57, no. 2, 659--676, 1992
Bounded linear logic: a modular approach to polynomial-time computability,
Theoret. Comput. Sci. 97, no. 1, 1--66, 1992
Le champ du signe,
Le théorème de Gödel, Le Seuil, Paris, 1989. Repris sous le titre : Il sogno del segno dans La prova di Gödel, Boringhieri, 1992
Logic and exceptions: a few remarks,
J. Logic Comput. 2, no. 2, 111--118, 1992
La mouche dans la bouteille [The fly in the bottle (in memory of Jean van Heijenoort)],
L'âne, octobre 1986 and also in Logic colloquium '85 (Orsay, 1985), 9--12, Stud. Logic Found. Math., 122, North-Holland, Amsterdam-New York, 1987 and Translated from the French by Thomas Drucker. Special issue: Jean van Heijenoort. Modern Logic 2, no. 3, 256--259, 1992
Normal forms and cut-free proofs as natural transformations,
Logic from computer science (Berkeley, CA, 1989), 217--241, Math. Sci. Res. Inst. Publ., 21, Springer, New York, 1992
Quantifiers in linear logic. II,
CLUEB, Nuovi problemi della logica e della filosofia della scienza, Corsi and Sambin, Editors, Bologna, pp. 79-90, 1991
Girard Jean-Yves
Introduction à la logique linéaire [Introduction
to linear logic],
Logique et informatique: une introduction, 229--256,
Collect. Didact., 8, INRIA, Rocquencourt, 1991
Girard Jean-Yves
A new constructive logic: classical logic,
Math. Structures Comput. Sci. 1, no. 3, 255--296,
1991
Some uses of dilators in combinatorial problems. II,
J. Symbolic Logic 55, no. 1, 32--40, 1990
Geometry of interaction. II. Deadlock-free algorithms,
COLOG-88 (Tallinn, 1988), 76--93, Lecture Notes in Comput. Sci., 417, Springer, Berlin, 1990
La logique linéaire,
Pour la Science, 150, 74-85, avril 1990
Bounded linear logic: a modular approach to polynomial time computability (extended abstract),
Feasible mathematics (Ithaca, NY, 1989), 195--209, Progr. Comput. Sci. Appl. Logic, 9, Birkh?ser Boston, Boston, MA, 1990
Quantifiers in linear logic. I,
CLUEB, Temi e prospettive della logica e della filosofia della scienza contemporanee, dalla Chiara and Galavotti Editors, Bologna, pp. 95-130, 1989
Semantic parametricity in typed lambda-calculus,
Logic and Computer Science 1988, IEEE Computer Society Press, Los Alamitos, pp. 69-108, 1989
Proofs and types,
Cambridge Tracts in Theoretical Computer Science, 7. Cambridge University Press, Cambridge-New York, 1989
Geometry of interaction. I. Interpretation of system F,
Logic Colloquium '88 (Padova, 1988), 221--260, Stud. Logic Found. Math., 127, North-Holland, Amsterdam, 1989
Towards a geometry of interaction,
Categories in computer science and logic (Boulder, CO, 1987), 69--108, Contemp. Math., 92, Amer. Math. Soc., Providence, RI, 1989
Sources et ressources de la théorie de la démonstration,
L'Ane, octobre 1989
La logique comme science de l'interaction,
Étude, UNESCO, Paris, mars 1988
Girard Jean-Yves
Multiplicatives,
Conference on Logic and Computer Science: New Trends
and Applications (Turin, 1986). Rend. Sem. Mat. Univ. Politec. Torino
1987, Special Issue, 11--33, 1988
Normal functors, power series and lambda-calculus,
Ann. Pure Appl. Logic 37, no. 2, 129--177, 1988
Mustard watches : an integrated approach to time and food,
Étude, UNESCO, Paris, mars 1988
Some uses of dilators in combinatorial problems. I,
Logic and combinatorics (Arcata, Calif., 1985), 25--53, Contemp. Math., 65, Amer. Math. Soc., Providence, R.I., 1987
Pi12-logic and related topics,
Proceedings of the conferences on mathematical logic, Vol. 3 (Italian) (Siena, 1985; Padova, 1985 and Siena, 1986), 13--45, Univ. Siena, 1987
Linear logic and parallelism,
Mathematical models for the semantics of parallelism (Rome, 1986), 166--182, Lecture Notes in Comput. Sci., 280, Springer, Berlin, 1987
Linear logic and lazy computation,
TAPSOFT '87, Vol. 2 (Pisa, 1987), 52--66, Lecture Notes in Comput. Sci., 250, Springer, Berlin-New York, 1987
Proof theory and logical complexity,
Studies in Proof Theory. Monographs, 1. Bibliopolis, Naples, 505, 1987
Le lambda-calcul du second ordre [The second-order lambda-calculus],
S?inaire Bourbaki, Vol. 1986/87. Ast?isque No. 152-153, 4, 173--186, 1987
L'infini en logique : autour du concept d'entier,
Enciclopedia Italiana, L'infinito nella scienza, Toraldo di Francia Editor, Roma, pp.141-150, 1987
Linear logic,
Theoret. Comput. Sci. 50, no. 1, 1--102, 1987
Logique et informatique : point de vue d'un logicien,
Étude, UNESCO, Paris, décembre 1986
Une théorie géométrique des ordinaux,
Pour la Science, juillet 1985. Repris dans Les Mathématiques d'Aujourd'hui, Belin, pp.97-108, 1986
The system F of variable types, fifteen years later,
Theoret. Comput. Sci. 45, no. 2, 159--192, 1986
Eléments de logique Pi1n [Elements of Pi1n-logic],
Recursion theory (Ithaca, N.Y., 1982), 389--445, Proc. Sympos. Pure Math., 42, Amer. Math. Soc., Providence, R.I., 1985
Introduction to Pi12-logic,
The present state of the problem of the foundations of mathematics (Florence, 1981). Synthese 62, no. 2, 191--216, 1985
Le rasoir de Kreisel,
L'Ane, juillet 1985
Set recursion and Pi12-logic,
Ann. Pure Appl. Logic 28, no. 3, 255--286, 1985
Functors and ordinal notations. II. A functorial construction of the Bachmann hierarchy,
J. Symbolic Logic 49, no. 4, 1079--1114, 1984
Functors and ordinal notations. I. A functorial construction of the Veblen hierarchy,
J. Symbolic Logic 49, no. 3, 713--729, 1984
Intuitionnisme,
Encyclœpedia Universalis, Paris, pp. 74-77, 1984
Théorie de la démonstration,
Encyclœpedia Universalis, Paris, pp. 1101-1105, 1984
The Omega-rule,
Proceedings of the International Congress of Mathematicians, Vol. 1, 2 (Warsaw, 1983), 307--321, PWN, Warsaw, 1984
Les premiers ordinaux récursivement inaccessible et Mahlo et la théorie des dilatateurs [The first recursively inaccessible and Mahlo numbers and the theory of dilators],
Arch. Math. Logik Grundlag. 24, no. 3-4, 167--191, 1984
Sur le théorème d'incomplétude de Gödel,
Cinq conférences sur l'indécidabilité, Bouleau Editor, Presses des Ponts & Chaussées, Paris, pp.25-48, 1983
A survey of Pi12-logic,
Logic, methodology and philosophy of science, VI (Hannover, 1979), pp. 89--107, Stud. Logic Foundations Math., 104, North-Holland, Amsterdam-New York, 1982
Proof-theoretic investigations of inductive definitions. I,
Logic and algorithmic (Zurich, 1980), pp. 207--236, Monograph. Enseign. Math., 30, Univ. Gen?e, Geneva, 1982
Herbrand's theorem and proof theory,
Proceedings of the Herbrand symposium (Marseilles, 1981), 29--38, Stud. Logic Found. Math., 107, North-Holland, Amsterdam-New York, 1982
A result on implications of
1-sentences
and its application to normal form theorems,J. Symbolic Logic 46, no. 3, 634--642, 1981
Pi12-logic. I. Dilators,
Ann. Math. Logic 21, no. 2-3, 75--219, 1981
Functionals and ordinoids,
Colloque International de Logique (Clermont-Ferrand, 1975), pp. 59--71, Colloq. Internat. CNRS, 249, CNRS, Paris, 1977
Functional interpretation and Kripke models,
Logic, foundations of mathematics and computability theory (Proc. Fifth Internat. Congr. Logic, Methodology and Philos. of Sci., Univ. Western Ontario, London, Ont., 1975), Part I, pp. 33--157. Univ. Western Ontario Ser. Philos. Sci., Vol. 9, Reidel, Dordrecht, 1977
Girard Jean-Yves
Three-valued logic and cut-elimination: the actual meaning of Takeuti's
conjecture,
Dissertationes Math. (Rozprawy Mat.) 136, 1--49,
1976
Quelques résultats sur les interprétations fonctionnelles,
Cambridge Summer School in Mathematical Logic (Cambridge, England, 1971), pp. 232--252. Lecture Notes in Math., Vol. 337, Springer, Berlin, 1973
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 of the Second Scandinavian Logic Symposium (Univ. Oslo, Oslo, 1970), pp. 63--92. Studies in Logic and the Foundations of Mathematics, Vol. 63, North-Holland, Amsterdam, 1971
