Some Aspects of Impredicativity

Longo, Giuseppe

Longo, Giuseppe

Séminaire de Philosophie et Mathématiques, no. 2 (1993), article no. 2, 19 p.

Export
Comment citer

@article{SPHM_1993___2_A2_0,
     author = {Longo, Giuseppe},
     title = {Some {Aspects} of {Impredicativity}},
     journal = {S\'eminaire de Philosophie et Math\'ematiques},
     eid = {2},
     pages = {10--28},
     publisher = {IREM Paris-Nord},
     number = {2},
     year = {1993},
     language = {en},
     url = {http://www.numdam.org/item/SPHM_1993___2_A2_0/}
}

TY  - JOUR
AU  - Longo, Giuseppe
TI  - Some Aspects of Impredicativity
JO  - Séminaire de Philosophie et Mathématiques
PY  - 1993
SP  - 10
EP  - 28
IS  - 2
PB  - IREM Paris-Nord
UR  - http://www.numdam.org/item/SPHM_1993___2_A2_0/
LA  - en
ID  - SPHM_1993___2_A2_0
ER  -

%0 Journal Article
%A Longo, Giuseppe
%T Some Aspects of Impredicativity
%J Séminaire de Philosophie et Mathématiques
%D 1993
%P 10-28
%N 2
%I IREM Paris-Nord
%U http://www.numdam.org/item/SPHM_1993___2_A2_0/
%G en
%F SPHM_1993___2_A2_0

Longo, Giuseppe. Some Aspects of Impredicativity. Séminaire de Philosophie et Mathématiques, no. 2 (1993), article  no. 2, 19 p. http://www.numdam.org/item/SPHM_1993___2_A2_0/

Bibliographie
Cité par

Amadio R., Bruce K., Longo G. [1986] "The finitary projections model and the solution of higher order domain equations" IEEE Conference on Logic in Computer Science, Boston, June 1986.

Amadio R., Longo G. [1986] "Type-free compiling of parametric Types" IFIP Conference Formal description of Programming Concepts Ebberup (DK), North Holland, 1987 (to appear). | MR

Asperti A., Longo G. [1991] Categories, Types and Structures, M.I.T. Press. | MR

Barendregt, H. [1984] The lambda calculus: its syntax and semantics, Revised edition, N. H.. | MR | Zbl

Berardi S. [1988] "DI-domains as a model for λβP and higher order functional languages" draft, CMU.

Breazu-Tannen V., Coquand T. [1987] "Extensional models for polymorphism" TAPSOFT-CFLP, Pisa. | MR | Zbl

Browder, F. [1983] The Mathematical Heritage of Henri Poincaré, Vol. 39, Proceedings of Symposia in Pure Mathematics, American Math Society. | Zbl

Brouwer L. [1923]. "On the significance of principle of excluded middle in mathematics, especialy in function theory." in van Heijenoort [1967], pp. 302-334.

Carboni A., Freyd P., Scedrov A. [1987] "A categorical approach to realizability and polymorphic types" 3rd ACM Symp. on Math. Found of Lang. Seman., New Orleans, LNCS vol. 298, Springer- Verlag. | Zbl

Cardelli L. [1986] "A polymorphic ;-calculus with Type:Type", Preprint, Syst Res. Center, Dig. Equip. Corp.

Cardelli L. [1988] "A Quest preview", Preprint, Syst. Res. Center, Dig. Equip. Corp.

Cardelli L., Longo G. [1991] "A semantic basis for Quest", Journal of Functional Programming, vol. 1, n. 2, 1991 (pp.417-458). | MR | Zbl

Chandarasekharan, K. [1986] Hermann Weyl, Springer-Verlag, Berlin Heidelberg, Germany.

Coquand T., Gunter C., Winskel G.[1988] "Domain theoretic models of polymorphism" Info&Comp.. (to appear). | MR | Zbl

Ehrhard, T. [1988] "A Categorical Semantics of Constructions" Proceedings of L. I. C. S. '88, Edinburgh.

Feferman, S. [1964 "Systems of predicative analysis" JSL 29, 1-30. | MR | Zbl

Feferman, S. [1968] "Autonomous Transfinite Progressions and the Extent of Predicative Mathematics." In Logic, Methodology and Philosophy of Science III (Rootsellar, ed.), 121-135. | MR | Zbl

Feferman, S. [1975] "A language and axioms for explicit mathematics", in Lecture Notes in Mathematics 450, Springer-Verlag, pp. 87-139. | MR | Zbl

Feferman, S. [1984] "Foundational ways", in Perspectives in Mathematics (Birkha^ser, Basel), 147- 158. | MR | Zbl

Feferman, S. [1986] "Infinity in mathematics: is Cantor necessary?, in (Toraldo di Francia, G., ed.) L'infinito nella scienza/ Infinity in science, Enciclopedia Italiana (Rome), 151-210.

Feferman, S. [1987] "Weyl Vindicated: "Das Kontinuum" 70 Years Later", preprint, Stanford University (Proceedings of the Cesena Conference in Logic and Philosophy of Science, to appear).

Girard, J. [1972] "Interpretation fonctionelle et elimination des coupure dans l'arithmetic d'ordre superieur," These de Doctorat d'Etat, Paris.

Girard J.Y. [1986] The system F of variable types, fifteen years later" Theor. comp. Sci, vol. 45, pp. 159-192. | MR | Zbl

Goldfarb, W. [1986] "Poincare Against the Logicists" to appear W. Aspray and P.Kitcher, Essays in the History and Philosophy of Mathematics, (Minn. Studies in the Phil, of Science). | MR

Harper R., Honsell F., Plotkin G. [1987] "A framework for defining logics" LICS 87, Cornell. | Zbl

Van Heijenoort, J. [1967] From Frege to Godel, Harvard University Press. Cambridge, Massachusetts. | Zbl

Hilbert D. [1925] "On the infinite" in van Heijenoort [1967], pp. 367-392.

Hilbert D. [1927] "The foundations of mathematics." in van Heijenoort [1967], pp. 464-480.

Hindley R., Longo G. [1980] "Lambda-calculus models and extensionality," Zeit. Math. Logik Grand. Math. n. 2, vol. 26 (289-310). | MR | Zbl

Hyland M. [1982] "The effective Topos," in The Brouwer Symposium, (Troelstra, Van Dalen eds.) North-Holland. | MR | Zbl

Hyland M. [1987] "A small complete category" Lecture delivered at the Conference Church's Thesis after 50 years, Zeiss (NL), June 1986 (Ann. Pure Appl. Logic, to appear). | MR | Zbl

Hyland M., Pitts A. [1987] "The Theory of Constructions: categorical semantics and topos theoretic models" Categories in Comp. Sci. and Logic, Boulder (AMS notes). | Zbl

Klop J.W. [1980] "Combinatory reduction systems" Thesis, Univ. Utrecht; publ. Math Centre, Kruislaan 413, Amsterdam, Holland. | MR | Zbl

Kreisel, G. [1960] "La Predicativit" In Bull. Soc math. France. 88, 1960, p. 371 a 391. | Numdam | MR | Zbl

Kreisel, G. [1968] "Functions, Ordinals, Species." In Logic, Methodology and Philosophy of Science III (Rootsellar, ed.), pp. 145-159. | MR | Zbl

Longo G. [1987] "On Church's Formal Theory of functions and functionals," Lecture delivered at the Conference Church's Thesis after 50 years, Zeiss (NL), June 1986 (Ann. Pure Appl. Logic, to appear). | MR

Longo, G. [1988] "From type-structures to Type Theories" notes for a graduate course at Carnegie Mellon University.

Longo G., Moggi E. [1988] "Constructive Natural Deduction and its ω-set Interpretation" Mathematical Structures in Computer Science, vol. 1, n. 2,1991 (pp. 215-253). | MR | Zbl

Longo G., Moggi E. [1989] "A category-theoretic characterization of functional completeness" Theor. Com. Sci. vol. 70, 2, 1990 (pp. 193-211). | MR | Zbl

Martini S. [1988] "Modelli non estensionali del polimorfismo in programmazione funzionale" Tesi di Dottorato, Pisa (in part to appear in the LISP Conference, 1988).

Martin-Löf P. [1984] Intuitionistic Type Theory, Bibliopolis, Napoli. | MR

Meyer A. R., Mitchell J., Moggi E., Statman R. [1987] "Empty types in polymorphic lambda calculus" (ACM Conference on) POPL '87, Munich.

Meyer, A. R. Reinhold, M.B. [1986] "Type is not a type", (ACM Conference on) POPL '86.

Mitchell J. [1986] "A type-inference approach to reduction properties and semantics of polymorphic expressions" ACM Conference on LISP and Functional Programming, Boston.

Mitchell J. C., Plotkin G. [1985] "Abstract types have exixtential types" Proc. Popl 85, ACM.

Pitts A. [1987] "Polymorphism is set-theoretic, constructively" Symposium on Category Theory and Comp. Sci., SLNCS 283 (Pitt et al. eds), Edinburgh. | MR | Zbl

Poincaré, H. [1913] Derni <res Pens> es, (english edition, Dover Publ., Inc., New York, 1963).

Reynolds J. [1984], "Polymorphism is not set-theoretic," Symposium on Semantics of Data Types, (Kahn, MacQueen, Plotkin, eds.) LNCS 173, Springer-Verlag | MR | Zbl

Rosolini G. [1986th] "Continuity and efffectiveness in Topoi" D. Phil. Thesis, Oxford Univ.

Rosolini G. [1986] "About Modest Sets" Notes for a talk delivered in Pisa. | Zbl

Scott D. [1972] "Continuous lattices" Toposes, algebraic Geometry and Logic, (Lawvere ed.), SLNM 274, (pp.97-136) Springer-Verlag. | MR | Zbl

Scott D. [1976] "Data types as lattices," SIAM Journal of Computing, 5 (pp. 522-587). | MR | Zbl

Scott D. [1980] "A space of retracts" Manuscript, Bremen.

Scott, D. [1982] "Some ordered sets in Computer Science," in Ordered Sets (Rival Ed.), Reidel. | MR | Zbl

Seely, R. [1987] "Categorical semantics for higher order polymorphic lambda calculus", JSL, vol. 52, n. 4, pp. 969-989. | MR | Zbl

Tonietti T. [1981] "Inspired Mathematics or Applied Mathematics ? (Epistemological and historical notes on Catastrophe Controversy)" Fundamenta Scientiae vol. 2, n.3/4, pp. 321-343. | MR

Troesltra A.S. [1973] "Notes in intutionistic second order arithmetic," Cambridge Summer School in Mathematical Logic, Springer LNM 337, pp. 171-203. | MR | Zbl

Weyl, H. [1918] Das Kontinuum, (italian edition, care of B. Veit, Bibliopolis, Napoli, 1977).

Weyl, H. [1927] "Comments on Hubert's second lecture on the foundations of mathematics." in van Heijenoort [1967]

Weyl, H. [1934] Mind and Nature, Univ. of Pennsylvania publ.. | JFM | MR

Weyl, H. [1949] Philosophy of Mathematics and Natural Science, Princeton University Press, Princeton, New Jersey. | MR | Zbl

Weyl, H. [1952] Symmetry, Princeton University Press, Princeton, New Jersey. | MR | Zbl

Weyl, H. [1985] "Axiomatic Versus Constructive Procedures in Mathematics." (Edited by T. Tonietti) The Mathematical Intelligence Vol. 7, No. 4, Springer-Verlag New York. | MR | Zbl