Practical Foundations of Mathematics

Paul Taylor

Chapter 9
Bibliography

[AJ94]
Samson Abramsky and Achim Jung. Domain theory. In Samson Abramsky et al., editors, Handbook of Logic in Computer Science, volume 3, pages 1-168. Oxford University Press, 1994.

[Acz88]
Peter Aczel. Non-well-founded Sets. Number 14 in Lecture Notes. Center for the Study of Language and Information, Stanford University, 1988.

[AR94]
Ji ri Adámek and Ji ri Rosický. Locally Presentable and Accessible Categories. Number 189 in London Mathematical Society Lecture Notes. Cambridge University Press, 1994.

[Age92]
Pierre Ageron. The logic of structures. Journal of Pure and Applied Algebra, 79:15-34, 1992.

[AHS95]
Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction-free normalisation proof. In Peter Johnstone, David Pitt, and David Rydeheard, editors, Category Theory and Computer Science VI, number 953 in Lecture Notes in Computer Science, pages 182-199. Springer-Verlag, 1995.

[AC98]
Roberto Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi. Number 46 in Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1998.

[App92]
Andrew Appel. Compiling with Continuations. Cambridge University Press, 1992.

[AGV64]
Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier, editors. Séminaire de Géometrie Algébrique, IV: Théorie des Topos, numbers 269-270 in Lecture Notes in Mathematics. Springer-Verlag, 1964. Second edition, 1972.

[Bae97]
John Baez. An introduction to n-categories. In Eugenio Moggi and Giuseppe Rosolini, editors, Category Theory and Computer Science VII, number 1290 in Lecture Notes in Computer Science, pages 1-33. Springer-Verlag, 1997.

[Bar81]
Henk Barendregt. The Lambda Calculus: its Syntax and Semantics. Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1981. Second edition, 1984.

[Bar92]
Henk Barendregt. Lambda calculi with types. In Samson Abramsky et al., editors, Handbook of Logic in Computer Science, volume 2, pages 117-309. Oxford University Press, 1992.

[BHPRR66]
Yehoshua Bar-Hillel, E. I. J. Poznanski, M. O. Rabin, and Abraham Robinson, editors. Essays of the Foundations of Mathematics . Magnes Press, Hebrew University, 1966. Distributed by Oxford University Press.

[BB69]
Michael Barr and Jon Beck. Homology and standard constructions. In Eckmann [Eck69], pages 245-335.

[BGvO71]
Michael Barr, Pierre Grillet, and Donovan van Osdol, editors. Exact Categories and Categories of Sheaves. Number 236 in Lecture Notes in Mathematics. Springer-Verlag, 1971.

[Bar79]
Michael Barr. *-Autonomous Categories. Number 752 in Lecture Notes in Mathematics. Springer-Verlag, 1979.

[BW85]
Michael Barr and Charles Wells. Toposes, Triples, and Theories. Number 278 in Grundlehren der mathematischen Wissenschaften. Springer-Verlag, 1985.

[BW90]
Michael Barr and Charles Wells. Category Theory for Computing Science. International Series in Computer Science. Prentice-Hall, 1990. Second edition, 1995.

[Bar91]
Michael Barr. *-Autonomous categories and linear logic. Mathematical Structures in Computer Science, 1:159-178, 1991.

[Bar77]
Jon Barwise, editor. Handbook of Mathematical Logic. Number 90 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1977.

[Bee80]
Michael Beeson. Foundations of Constructive Mathematics: Metamathematical Studies. Number 6 in Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer-Verlag, 1980. Second edition, 1985.

[Bel88]
John Lane Bell. Toposes and Local Set Theories: an Introduction. Number 14 in Logic Guides. Oxford University Press, 1988.

[Bén85]
Jean Bénabou. Fibred categories and the foundations of naive category theory. Journal of Symbolic Logic, 50:10-37, 1985.

[BP64]
Paul Benacerraf and Hilary Putnam, editors. Philosophy of Mathematics: Selected Readings. Prentice-Hall, 1964. Second edition, Cambridge University Press, 1983.

[Ben64]
Paul Benacerraf. What numbers could not be. In Benacerraf and Putnam [BP64], pages 272-294. Second edition, Cambridge University Press, 1983.

[Ber35]
Paul Bernays. Sur le platonisme dans les mathématiques. Enseignement Mathématique, 34:52-69, 1935. English translation, ``Platonism in Mathematics'' in [ BP64], pages 258-271.

[Bib82]
Wolfgang Bibel. Automated Theorem Proving. Friedrich Vieweg & Sohn, Braunschweig, 1982. Second edition, 1987.

[BML41]
Garrett Birkhoff and Saunders Mac Lane. A Survey of Modern Algebra. MacMillan, New York, 1941. Fourth edition, 1977.

[Bir76]
Garrett Birkhoff. The rise of modern algebra. In Jan Dalton Tarwater, John White, and John Miller, editors, Men and Institutions in American Mathematics, pages 41-86. Texas Technical University, 1976.

[BB85]
Errett Bishop and Douglas Bridges. Constructive Analysis. Number 279 in Grundlehren der mathematischen Wissenschaften. Springer-Verlag, 1985.

[Bla33]
Max Black. The Nature of Mathematics, a Critical Survey. International Library of Psychology. Kegan Paul, 1933.

[Boc51]
Josef Bochenski. Ancient Formal Logic. Studies in Logic and the Foundations of Mathematics. North-Holland, 1951.

[Boe52]
Philotheus Boehner. Medieval Logic: an Outline of its Development from 1250 to c.1400. Manchester University Press, 1952.

[Boe58]
Philotheus Boehner. Collected articles on Ockham. Franciscan Institute, 1958. Edited by Elio Marie Buytaert.

[Bol51]
Bernard Bolzano. Paradoxien des Undlichen. 1851. English translation, ``Paradoxes of the Infinite'' by Fr. Prihonsky, published by Routledge, 1950.

[BJ74]
George Boolos and Richard Jeffrey. Computability and Logic. Cambridge University Press, 1974. Third edition, 1989.

[Boo93]
George Boolos. The Logic of Provability. Cambridge University Press, 1993.

[Boo98]
George Boolos. Logic, Logic and Logic. Harvard University Press, 1998. Edited by Richard Jeffrey.

[Bor94]
Francis Borceux. Handbook of Categorical Algebra. Number 50 in Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994. Three volumes.

[Bou57]
Nicolas Bourbaki. Eléments de Mathématique XXII: Théories des Ensembles, Livre I, Structures. Number 1258 in Actualités scientifiques et industrielles. Hermann, 1957. English translation, ``Theory of Sets,'' 1968.

[Boy68]
Carl Boyer. A History of Mathematics. Wiley, 1968. Revised edition by Uta Merzbach, Wiley, 1989.

[BM88]
Robert Boyer and J. Strother Moore. A Computational Logic Handbook. Number 23 in Perspectives in Computing. Academic Press, 1988.

[Bro75]
Jan Brouwer. Collected Works: Philosophy and Foundations of Mathematics, volume 1. North-Holland, 1975. Edited by Arend Heyting.

[Bro81]
Jan Brouwer. Brouwer's Cambridge Lectures on Intuitionism . Cambridge University Press, 1981. Edited by Dirk van Dalen.

[Bro76]
Felix Browder, editor. Mathematical Developments Arising from Hilbert Problems, number 28 in Proceedings of Symposia in Pure Mathematics. American Mathematical Society, 1976.

[Bro87]
Ronald Brown. From groups to groupoids: a brief survey. Bulletin of the London Mathematical Society, 19:113-134, 1987.

[Bro88]
Ronald Brown. Topology: a Geometric Account of General Topology, Homotopy Types and the Fundamental Groupoid. Mathematics and its Applications. Ellis Horwood, 1988. First edition ``Elements of modern topology,'' 1968.

[BS81]
Stanley Burris and H. P. Sankappanavar. A Course in Universal Algebra. Number 78 in Graduate Texts in Mathematics. Springer-Verlag, 1981.

[Bur81]
Albert Burroni. Algèbres graphiques. Cahiers de Topologie et Géométrie Différentielle, XXII, 1981.

[Caj93]
Florian Cajori. A History of Mathematics. MacMillan, 1893. Fifth edition, Chelsea, N.Y., 1991.

[Caj28]
Florian Cajori. A History of Mathematical Notations. Open Court, 1928. Reprinted by Dover, 1993.

[Cam98]
Peter Cameron. Introduction to Algebra. Oxford University Press, 1998.

[Can15]
Georg Cantor. Contributions to the Founding of the Theory of Transfinite Numbers. Open Court, 1915. Translated and edited by Philip Jourdain; reprinted by Dover, 1955.

[Can32]
Georg Cantor. Gesammelte Abhandlungen mathematischen und philosophischen Inhalts. Springer-Verlag, 1932. Edited by Ernst Zermelo; reprinted by Olms, Hildeshaim, 1962.

[CPR91]
Aurelio Carboni, Maria-Cristina Peddicchio, and Giuseppe Rosolini, editors. Proceedings of the 1990 Como Category Theory Conference, number 1488 in Lecture Notes in Mathematics. Springer-Verlag, 1991.

[CLW93]
Aurelio Carboni, Steve Lack, and Robert Walters. Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra, 84:145-158, 1993.

[Car34]
Rudolf Carnap. Logische Syntax der Sprache. Vienna, 1934. English translation by Amethe Smeaton, ``The Logical Syntax of Language,'' Kegan Paul, 1937.

[CE56]
Henri Cartan and Sammy Eilenberg. Homological Algebra. Princeton University Press, 1956.

[Car86]
John Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209-243, 1986.

[CK73]
Chen Chung Chang and Jerome Keisler. Model Theory. Number 73 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1973. Third edition, 1990.

[CR92]
Jon Chapman and Frederick Rowbottom. Relative Category Theory and Geometric Morphisms: a Logical Approach. Number 16 in Logic Guides. Oxford University Press, 1992.

[Chu56]
Alonso Church. Introduction to Mathematical Logic. Princeton University Press, 1956.

[Coc93]
Robin Cockett. Introduction to distributive categories. Mathematical Structures in Computer Science, 3:277-307, 1993.

[CCS98]
A. M. Cohen, H. Cuypers, and H. Sterk, editors. Some Tapas of Computer Algebra, number 4 in Algorithms and Computation in Mathematics. Springer-Verlag, 1998.

[Coh66]
Paul Cohen. Set Theory and the Continuum Hypothesis. W.A. Benjamin, 1966.

[Coh77]
Paul Cohn. Algebra, volume 2. Wiley, 1977.

[Coh81]
Paul Cohn. Universal Algebra. Number 6 in Mathematics and its Applications. Reidel, 1981. Originally published by Harper and Row, 1965.

[Con71]
John Horton Conway. Regular Algebra and Finite Machines. Chapman and Hall, 1971.

[Con76]
John Horton Conway. On Numbers and Games. Number  6 in London Mathematical Society Monographs. Academic Press, 1976.

[CH88]
Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76:95-120, 1988.

[Coq90a]
Thierry Coquand. Metamathematical investigations of a calculus of constructions. In Odifreddi [ Odi90], pages 91-122.

[Coq90b]
Thierry Coquand. On the analogy between propositions and types. In Gérard Huet, editor, Logical Foundations of Functional Programming, pages 399-418. Addison-Wesley, 1990.

[Coq97]
Thierry Coquand. Computational content of classical logic. In Pitts and Dybjer [PD97], pages 33-78.

[Cos79]
Michel Coste. Localisation, spectra and sheaf representation. In Fourman et al. [ FMS79], pages 212-238.

[Cou05]
Louis Couturat. Les Principes des Mathématiques, avec un Appendice sur le Philosophie de Kant. 1905.

[CP92]
Roy Crole and Andrew Pitts. New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic. Information and Computation, 98:171-210, 1992.

[Cro93]
Roy Crole. Categories for Types. Cambridge Mathematical Textbooks. Cambridge University Press, 1993.

[CDS98]
Djordje Cubri\'c, Peter Dybjer, and Philip Scott. Normalisation and the Yoneda embedding. Mathematical Structures in Computer Science, 8:153-192, 1998.

[Cur86]
Pierre-Louis Curien. Categorical Combinators, Sequential Algorithms, and Functional Programming. Pitman, 1986. Second edition, Birkhäuser, Progress in Theoretical Computer Science, 1993.

[CF58]
Haskell Curry and Robert Feys. Combinatory Logic I. Studies in Logic and the Foundations of Mathematics. North- Holland, 1958. Volume II, with Jonathan Seldin, 1972.

[Cur63]
Haskell Curry. Foundations of Mathematical Logic. McGraw-Hill, 1963. Republished by Dover, 1977.

[CSH80]
Haskell Curry, Jonathan Seldin, and Roger Hindley, editors. To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.

[Dau79]
Joseph Warren Dauben. Georg Cantor: his Mathematics and Philosophy of the Infinite. Harvard University Press, 1979.

[DST88]
James Davenport, Y. Siret, and E. Tournier. Computer Algebra: Systems and Algorithms for Algebraic Computation. Academic Press, 1988. Translated from French; third edition 1993.

[DP90]
B. A. Davey and Hilary Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.

[Dav65]
Martin Davis. The Undecidable. Basic Papers on Undecidable, Unsolvable Problems and Computable Functions. Raven Press, Hewlett, N.Y., 1965.

[dB80]
Nikolas de Bruijn. A survey of the project Automath. In Curry et al. [CSH80], pages 579-606.

[Ded72]
J. W. Richard Dedekind. Stetigkeit und irrationale Zahlen. Braunschweig, 1872. Reprinted in [Ded32], pages 315-334; English translation, ``Continuity and Irrational Numbers'' in [Ded01].

[Ded88]
J. W. Richard Dedekind. Was sind und was sollen die Zahlen? Braunschweig, 1888. Reprinted in [Ded32], pages 335-391; English translation, ``The Nature and Meaning of Numbers'' in [Ded01].

[Ded01]
J. W. Richard Dedekind. Essays on the theory of numbers. Open Court, 1901. English translations by Wooster Woodruff Beman; republished by Dover, 1963.

[Ded32]
J. W. Richard Dedekind. Gesammelte mathematische Werke, volume 3. Vieweg, Braunschweig, 1932. Edited by Robert Fricke, Emmy Noether and Ø ystein Ore; republished by Chelsea, New York, 1969.

[Det86]
Michael Detlefsen. Hilbert's Program: an Essay on Mathematical Instrumentalism. Number 182 in Synthese Library. Reidel, 1986.

[Die77]
Jean Alexandre Dieudonné. Panorama des Mathé matiques Pures: la Choix Bourbachique. Gauthier-Villars, 1977. English translation, ``A panorama of pure mathematics, as seen by N. Bourbaki'' by I. G. Macdonald, Academic Press, Pure and applied mathematics, 97, 1982.

[Die88]
Jean Alexandre Dieudonné. A History of Algebraic and Differential Topology 1900-1960. Birkhäuser, 1988.

[Dol72]
Albrecht Dold. Lectures on Algebraic Topology. Number 200 in Grundlehren der mathematischen Wissenschaften. Springer- Verlag, 1972.

[Dum77]
Michael Dummett. Elements of Intuitionism. Logic Guides. Oxford University Press, 1977.

[Dum78]
Michael Dummett. Truth and Other Enigmas. Duckworth, London, 1978.

[DT87]
Roy Dyckhoff and Walter Tholen. Exponentiable maps, partial products and pullback complements. Journal of Pure and Applied Algebra, 49:103-116, 1987.

[Eck69]
Beno Eckmann, editor. Seminar on Triples and Categorical Homology Theory, number 80 in Lecture Notes in Mathematics. Springer- Verlag, 1969.

[Ehr84]
Charles Ehresman. OEuvres complètes et commentées. Amiens, 1980-84. Edited by Andrée Charles Ehresmann; published as supplements to volumes 21-24 of Cahiers de topologie et géométrie différentielle.

[Ehr88]
Thomas Ehrhardt. Categorical semantics of constructions. In Yuri Gurevich, editor, Logic in Computer Science III, pages 264-273. IEEE Computer Society Press, 1988.

[Ehr89]
Thomas Ehrhardt. Dictoses. In Pitt et al. [ PRD+89], pages 213-223.

[ES52]
Sammy Eilenberg and Norman Steenrod. Foundations of Algebraic Topology. Princeton University Press, 1952.

[EHMLR66]
Sammy Eilenberg, D. K. Harrison, Saunders Mac Lane, and Helmut Röhrl, editors. Categorical Algebra (La Jolla, 1965). Springer- Verlag, 1966.

[EK66]
Sammy Eilenberg and Max Kelly. Closed categories. In Eilenberg et al. [EHMLR66].

[EE70]
Sammy Eilenberg and Calvin Elgot. Recursiveness. Academic Press, 1970.

[EML86]
Sammy Eilenberg and Saunders Mac Lane. Eilenberg-Mac Lane, Collected Works. Academic Press, 1986.

[FG87]
John Fauvel and Jeremy Gray. The History of Mathematics, a Reader. Macmillan and the Open University, 1987.

[Fen71]
Jens Erik Fenstad, editor. Second Scandinavian Logic Symposium, number 63 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1971.

[FF69]
Richard Feys and Frederic Fitch. Dictionary of Symbols of Mathematical Logic. Studies in Logic and the Foundations of Mathematics. North-Holland, 1969.

[FJM +96]
Marcelo Fiore, Achim Jung, Eugenio Moggi, Peter O'Hearn, Jon Riecke, Giuseppe Rosolini, and Ian Stark. Domains and denotational semantics: History, accomplishments and open problems. Bulletin of the EATCS, 59:227-256, 1996.

[Fit52]
Frederic Benton Fitch. Symbolic Logic: an Introduction. Ronald Press, New York, 1952.

[Fit69]
Melvin Fitting. Intuitionistic Logic, Model Theory and Forcing. Studies in Logic and the Foundations of Mathematics. North-Holland, 1969.

[Flo67]
Robert Floyd. Assigning meaning to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, number 19 in Proceedings of Symposia in Applied Mathematics, pages 19-32. American Mathematical Society, 1967.

[FMS79]
Michael Fourman, Chris Mulvey, and Dana Scott, editors. Applications of Sheaves, number 753 in Lecture Notes in Mathematics. Springer-Verlag, 1979.

[FJP92]
Michael Fourman, Peter Johnstone, and Andrew Pitts, editors. Applications of categories in computer science, number 177 in London Mathematical Society Lecture Notes. Cambridge University Press, 1992.

[Fow87]
David Fowler. The Mathematics of Plato's Academy: a New Reconstruction. Oxford University Press, 1987.

[FBH58]
Abraham Fraenkel and Yehoshua Bar-Hillel. Foundations of Set Theory. Studies in Logic and the Foundations of Mathematics . North-Holland, 1958.

[Fre60]
Gottlob Frege. Translations from the Philosophical Writings of Gottlob Frege. Blackwell, 1960. Edited by Peter Geach and Max Black; third edition, 1980.

[Fre84]
Gottlob Frege. Collected Papers on Mathematics, Logic and Philosophy. Blackwell, 1984. Edited by Brian McGinness.

[Fre64]
Peter Freyd. Abelian Categories: an Introduction to the Theory of Functors. Harper and Row, 1964.

[Fre66]
Peter Freyd. The theory of functors and models. In John Addison, Leon Henkin, and Alfred Tarski, editors, Theory of Models, Studies in Logic and the Foundations of Mathematics, pages 107-120. North-Holland, 1966.

[Fre72]
Peter Freyd. Aspects of topoi. Bulletin of the Australian Mathematical Society, 7:1-76 and 467-480, 1972.

[FK72]
Peter Freyd and Max Kelly. Categories of continuous functors, I . Journal of Pure and Applied Algebra, 2:169-191, 1972.

[FS90]
Peter Freyd and Andre Scedrov. Categories, Allegories. Number 39 in Mathematical Library. North-Holland, 1990.

[Fre91]
Peter Freyd. Algebraically complete categories. In Carboni et al. [CPR91], pages 95-104.

[GU71]
Peter Gabriel and Fritz Ulmer. Lokal präsentierbare Kategorien. Number 221 in Lecture Notes in Mathematics. Springer-Verlag, 1971.

[Gal38]
Galileo Galilei. Two New Sciences. 1638. Translated by Stillman Drake, University of Wisconsin Press, 1974; Re-published by Wall & Thompson, 1989.

[Gal86]
Jean Gallier. Logic for Computer Science: Foundations of Automated Theorem Proving. Computer Science and Technology Series. Harper and Row, 1986. Republished by Wiley, 1987.

[Gan56]
Robin Gandy. On the axiom of extensionality. Journal of Symbolic Logic, 21:36-48 and 24:287-300, 1956.

[Gen35]
Gerhard Gentzen. Untersuchungen über das Logische Schliessen. Mathematische Zeitschrift, 39:176-210 and 405-431, 1935. English translation in [ Gen69], pages 68-131.

[Gen69]
Gerhard Gentzen. The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics. North-Holland, 1969. Edited by M. E. Szabo.

[GHK +80]
Gerhard Gierz, Karl Heinrich Hoffmann, Klaus Keimel, Jimmie Lawson, Michael Mislove, and Dana Scott. A Compendium of Continuous Lattices. Springer-Verlag, 1980.

[Gil82]
Donald Gillies. Frege, Dedekind and Peano on the Foundations of Arithmetic. Number 2 in Methodology and Science Foundation. Van Gorcum, 1982.

[Gir71]
Jean-Yves Girard. Une extension de l'interpretation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types. In Fenstad [Fen71], pages 63-92.

[Gir87a]
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987.

[Gir87b]
Jean-Yves Girard. Proof Theory and Logical Complexity, volume 1. Bibliopolis, 1987.

[GLT89]
Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Number 7 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[Gir71]
Jean Giraud. Cohomologie non-abélienne. Number 179 in Grundlehren der mathematischen Wissenschaften. Springer- Verlag, 1971.

[Gir72]
Jean Giraud. Classifying topos. In Lawvere [ Law72], pages 43-56.

[Göd31]
Kurt Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38:173-198, 1931. English translations, ``On Formally Undecidable Propositions of `Principia Mathematica' and Related Systems'' published by Oliver and Boyd, 1962 and Dover, 1992; also in [vH67], pages 596-616 and [ Dav65], pages 5-38.

[Göd80]
Kurt Gödel. Kurt Gödel: Collected Works. Oxford University Press, 1980. Edited by Solomon Feferman and others.

[God58]
Roger Godement. Topologie Algebrique et Theorie des Faisceaux. Hermann, 1958.

[Gol79]
Robert Goldblatt. Topoi: The Categorial Analysis of Logic. Number 98 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1979. Third edition, 1983.

[GG80]
Ivor Grattan-Guinness, editor. From the Calculus to Set Theory, 1630-1910: an Introductory History. Duckworth, London, 1980.

[GG97]
Ivor Grattan-Guinness. The Fontana History of the Mathematical Sciences: the Rainbow of Mathematics. Fontana, 1997.

[Grä68]
George Grätzer. Universal Algebra. Van Nostrand, 1968.

[Gra66]
John Gray. Fibred and cofibred categories. In Eilenberg et al. [EHMLR66], pages 21-83.

[Gra79]
John Gray. Fragments of the history of sheaf theory. In Fourman et al. [FMS79], pages 1-79.

[GS89]
John Gray and Andre Scedrov, editors. Categories in Computer Science and Logic, number 92 in Contemporary Mathematics. American Mathematical Society, 1989.

[Gro64]
Alexander Grothendieck, editor. Séminaire de Géometrie Algébrique, I (1960/1), number 224 in Lecture Notes in Mathematics. Springer-Verlag, 1964.

[Gun92]
Carl Gunter. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing. MIT Press, 1992.

[Hal60]
Pál Halmos. Naive Set Theory. Van Nostrand, 1960. Reprinted by Springer-Verlag, Undergraduate Texts in Mathematics, 1974.

[Har40]
G. H. Hardy. A Mathematician's Apology. Cambridge University Press, 1940. Reprinted 1992.

[Hat82]
William Hatcher. The Logical Foundations of Mathematics. Foundations and Philosophy of Science and Technology. Pergamon Press, 1982.

[Hau14]
Felix Hausdorff. Mengenlehre. 1914. English translation, ``Set Theory,'' published by Chelsea, 1962.

[Hec93]
André Heck. Introduction to Maple. Springer-Verlag, 1993. Second edition, 1996.

[Hei86]
Gerhard Heinzmann, editor. Poincaré, Russell, Zermelo et Peano: Textes de la Discussion (1906-1912) sur les Fondements des Mathématiques: des Antinomies à la Prédicativité. Albert Blanchard, Paris, 1986.

[HM75]
Matthew Hennessey and Robin Milner. Algebraic laws for non- determinism and concurrency. Journal of the ACM, 32:137- 161, 1975.

[Hen88]
Matthew Hennessy. Algebraic Theory of Processes. Foundations of Computing. MIT Press, 1988.

[Hen90]
Matthew Hennessy. The Semantics of Programming Languages: an Elementary Introduction using Structural Operational Semantics. Wiley, 1990.

[Hey56]
Arend Heyting. Intuitionism, an Introduction. Studies in Logic and the Foundations of Mathematics. North-Holland, 1956. Revised edition, 1966.

[HA28]
David Hilbert and Wilhelm Ackermann. Grundzüge der theoretischen Logik. Springer-Verlag, 1928. Republished 1972; English translation by Lewis Hammond et al., ``Principles of Mathematical Logic,'' Chelsea, New York, 1950.

[HB34]
David Hilbert and Paul Bernays. Grundlagen der Mathematik . Number 40 in Grunlagen der Mathematischen Wissenschaften. Springer-Verlag, 1934.

[Hil35]
David Hilbert. Gesammelte Abhandlungen, volume 3. Springer-Verlag, 1935. Reprinted, 1970.

[HS71]
Peter Hilton and Urs Stammbach. A Course in Homological Algebra. Number 4 in Graduate Texts in Mathematics. Springer- Verlag, 1971. Second edition, 1997.

[HS86]
Roger Hindley and Jonathan Seldin. Introduction or Combinators and Lambda Calculus. Number 1 in London Mathematical Society Student Texts. Cambridge University Press, 1986.

[Hoa69]
Tony Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12:576-580 and 583, 1969.

[Hod93]
Wilfrid Hodges. Model Theory. Number 42 in Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993.

[Hof95]
Martin Hofmann. On the interpretation of type theory in locally cartesian closed categories. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic VIII, number 933 in Lecture Notes in Computer Science, pages 427-441. Springer-Verlag, 1995.

[Hof79]
Dougals Hofstadter. Gödel, Escher, Bach, and Eternal Golden Braid. Harvester, 1979. Reprinted by Penguin, 1980.

[How80]
William Howard. The formulae-as-types notion of construction. In Curry et al. [CSH80 ], pages 479-490.

[Hue73]
Gérard Huet. The undecidability of unification in third order logic. Information and Control, 22(3):257-267, April 1973.

[Hue75]
Gérard Huet. A unification algorithm for typed lambda calculus. Theoretical Computer Science, 1:27-57, 1975.

[HJP80]
Martin Hyland, Peter Johnstone, and Andrew Pitts. Tripos theory. Mathematical Proceedings of the Cambridge Philosophical Society, 88:205-232, 1980.

[Hyl81]
Martin Hyland. Function spaces in the category of locales. In Bernhard Banachewski and Rudolf-Eberhard Hoffman, editors, Continuous Lattices, number 871 in Lecture Notes in Mathematics, pages 264-281. Springer-Verlag, 1981.

[Hyl82]
Martin Hyland. The effective topos. In Troelstra and van Dalen [TvD82], pages 165-216.

[Hyl88]
Martin Hyland. A small complete category. Annals of Pure and Applied Logic, 40:135-165, 1988.

[HP89]
Martin Hyland and Andrew Pitts. The theory of constructions: Categorical semantics and topos-theoretic models. In Gray and Scedrov [GS89], pages 137-199.

[HRR90]
Martin Hyland, Edmund Robinson, and Giuseppe Rosolini. The discrete objects in the effective topos. Proceedings of the London Mathematical Society, 60:1-36, 1990.

[Jac90]
Bart Jacobs. Categorical Type Theory. PhD thesis, Universiteit Nijmegen, 1990.

[JMS91]
Bart Jacobs, Eugenio Moggi, and Thomas Streicher. Relating models of impredicative type theories. In Pitt et al. [ PCA+91], pages 197-218.

[Jac93]
Bart Jacobs. Comprehension categories and the semantics of type dependency. Theoretical Computer Science, 107(2):169-207, 1993.

[Jás34]
Stanislaw Jáskowski. On the rules of suppositions in formal logic. Studia Logica, 1, 1934. Reprinted in [McC67], pages 232-258.

[Jec78]
Thomas Jech. Set Theory. Number 79 in Pure and Applied Mathematics. Academic Press, 1978. Second edition, 1997.

[Joh77]
Peter Johnstone. Topos Theory. Number 10 in London Mathematical Society Monographs. Academic Press, 1977.

[JPR +78]
Peter Johnstone, Robert Paré, Robert Roseburgh, Steve Schumacher, Richard Wood, and Gavin Wraith. Indexed Categories and their Applications. Number 661 in Lecture Notes in Mathematics. Springer-Verlag, 1978.

[Joh82]
Peter Johnstone. Stone Spaces. Number 3 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.

[Joh85]
Peter Johnstone. When is a variety a topos? Algebra Universalis, 21:198-212, 1985.

[Joh90]
Peter Johnstone. Collapsed toposes and cartesian closed varieties. Journal of Algebra, 129:446-480, 1990.

[JT84]
André Joyal and Myles Tierney. An extension of the Galois theory of Grothendieck. Memoirs of the American Mathematical Society, 51(309), 1984.

[Joy87]
André Joyal. Foncteurs analytiques et espèces de structures. In Gilbert Labelle and Pierre Leroux, editors, Combinatoire énumerative, number 1234 in Lecture Notes in Mathematics, pages 126-159. Springer- Verlag, 1987.

[JM95]
André Joyal and Ieke Moerdijk. Algebraic Set Theory. Number 220 in London Mathematical Society Lecture Notes. Cambridge University Press, 1995.

[Jun90]
Achim Jung. Cartesian closed categories of algebraic CPO's. Theoretical Computer Science, 70:233-250, 1990.

[KR91]
Hans Kamp and Uwe Reyle. From Discourse to Logic: Introduction to Model-theoretic Semantics of Natural Language, Formal Logic and Discourse Representation Theory. Reidel, 1991. Re- published by Kluwer, Studies in Linguistics and Philosophy, 42, 1993.

[Kan58]
Daniel Kan. Adjoint functors. Transactions of the American Mathematical Society, 87:294-329, 1958.

[Kel55]
John Kelley. General Topology. Van Nostrand, 1955. Reprinted by Springer-Verlag, Graduate Texts in Mathematics, 27, 1975.

[Kel69]
Max Kelly. Monomorphisms, epimorphisms and pull-backs. Journal of the Australian Mathematical Society, 9:124-142 , 1969.

[Kel74]
Max Kelly, editor. Proceedings of the Sydney Category Theory Seminar 1972-3. Number 420 in Lecture Notes in Mathematics. Springer-Verlag, 1974.

[Kel82]
Max Kelly. Basic Concepts of Enriched Category Theory. Number 64 in London Mathematical Society Lecture Notes. Cambridge University Press, 1982.

[Kle52]
Stephen Kleene. Introduction to Metamathematics. Number 1 in Bibliotheca mathematica. North-Holland, 1952. Revised edition, Wolters-Noordhoff, 1971.

[KV65]
Stephen Kleene and Richard Vesley. The Foundations of Intuitionistic Mathematics, Especially in relation to Recursive Functions. North-Holland, 1965.

[Kle67]
Stephen Kleene. Mathematical Logic. John Wiley and Sons, 1967.

[Knu68]
Donald Knuth. The Art of Computer Programming. Addison-Wesley, 1968. Three volumes published out of seven planned; second edition, 1973.

[KB70]
Donald Knuth and Peter Bendix. Simple word problems in universal algebra. In John Leech, editor, Computational Problems in Abstract Algebra, pages 263-297. Pergamon Press, 1970.

[Knu74]
Donald Knuth. Surreal Numbers. Addison-Wesley, 1974.

[Koc81]
Anders Kock. Synthetic Differential Geometry. Number 51 in London Mathematical Society Lecture Notes. Cambridge University Press, 1981.

[Koc95]
Anders Kock. Monads for which structures are adjoint to units. Journal of Pure and Applied Algebra, 104:41-59, 1995.

[Kol25]
Andrei Kolmogorov. On the principle of excluded middle. Matemati ceskii Sbornik, 32:646-667, 1925. In Russian; English translation in [vH67 ], pages 414-437.

[Koy82]
C. P. J. Koymans. Models of the lambda calculus. Information and Control, 52:206-332, 1982.

[Kre58]
Georg Kreisel. Mathematical significance of consistency proofs. Journal of Symbolic Logic, 23:155-182, 1958.

[Kre67]
Georg Kreisel. Informal rigour and completeness proofs. In Imre Lakatos, editor, Problems in the Philosophy of Mathematics. North-Holland, 1967.

[Kre68]
Georg Kreisel. A survey of proof theory. Journal of Symbolic Logic, 33:321-388, 1968.

[Kre71]
Georg Kreisel. A survey of proof theory II. In Fenstad [Fen71], pages 109-170.

[KKP82]
Norman Kretzmann, Anthony Kenny, and Jan Pinborg, editors. The Cambridge history of later medieval philosophy: from the rediscovery of Aristotle to the disintegration of scholasticism, 1100-1600 . Cambridge University Press, 1982.

[KM66]
Kazimierz Kuratowski and Andrzej Mostowski. Teoria mnogosci. Polish Scientific Publishers, 1966. English translation, ``Set Theory'' by M. Maczynski, North-Holland, Studies in Logic and the Foundations of Mathematics, number 86, 1968; second edition, 1976.

[Laf87]
Yves Lafont. Logiques, Catégories et Machines. PhD thesis, Université de Paris 7, 1987.

[LS91]
Yves Lafont and Thomas Streicher. Game semantics for linear logic. In Logic in Computer Science VI, pages 43-50. IEEE Computer Society Press, 1991.

[Lai83]
Christian Lair. Diagrammes localement libres, extensions de corps et théorie de Galois. Diagrammes, 10, 1983.

[Lak63]
Imre Lakatos. Proofs and refutations: the logic of mathematical discovery. British Journal for the Philosophy of Science, 14:1-25, 1963. Edited by John Worrall and Elie Zahar, Cambridge University Press, 1976.

[Lak86]
George Lakoff. Women, Fire, and Dangerous Things: What Categories Reveal about the Mind. University of Chicago Press, 1986.

[Lam58]
Joachim Lambek. The mathematics of sentence structure. American Mathematical Monthly, 65:154-170, 1958.

[Lam68]
Joachim Lambek. Deductive systems and categories I: Syntactic calculus and residuated categories. Mathematical Systems Theory, 2:287-318, 1968.

[Lam69]
Joachim Lambek. Deductive systems and categories II: Standard constructions and closed categories. In Peter Hilton, editor, Category Theory, Homology Theory and their Applications, number 86 in Lecture Notes in Mathematics, pages 76-122. Springer-Verlag, 1969.

[Lam72]
Joachim Lambek. Deductive systems and categories III: Cartesian closed categories, intuitionist propositional calculus, and combinatory logic. In Lawvere [ Law72], pages 57-82.

[LS80]
Joachim Lambek and Philip J. Scott. Intuitionist type theory and the free topos. Journal of Pure and Applied Algebra, 19:215-257, 1980.

[LS86]
Joachim Lambek and Philip Scott. Introduction to Higher Order Categorical Logic. Number 7 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1986.

[Lam89]
Joachim Lambek. Multicategories revisited. In Gray and Scedrov [GS89], pages 217-240.

[Lan70]
Serge Lang. Introduction to linear algebra. Addison-Wesley, 1970. Third edition, Springer-Verlag, Undergraduate Texts in Mathematics, 1987.

[Law63]
Bill Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences of the United States of America, 50(1):869-872, 1963.

[Law64]
Bill Lawvere. An elementary theory of the category of sets. Proceedings of the National Academy of Sciences of the United States of America, 52:1506-1511, 1964.

[Law66]
William Lawvere. The category of categories as a foundation for mathematics. In Eilenberg et al. [ EHMLR66], pages 1-20.

[Law68a]
Bill Lawvere. Diagonal arguments and cartesian closed categories . In Peter Hilton, editor, Category Theory, Homology Theory and their Applications II, number 92 in Lecture Notes in Mathematics, pages 134-145. Springer-Verlag, 1968.

[Law68b]
Bill Lawvere. Some algebraic problems in the context of functorial semantics of algebraic structures. In Saunders Mac Lane, editor, Reports of the Midwest Category Seminar II, number 61 in Lecture Notes in Mathematics, pages 41-61. Springer-Verlag, 1968.

[Law69]
Bill Lawvere. Adjointness in foundations. Dialectica, 23:281-296, 1969.

[Law70]
Bill Lawvere. Equality in hyperdoctrines and the comprehension schema as an adjoint functor. In Alex Heller, editor, Applications of Categorical Algebra, number 17 in Proceedings of Symposia in Pure Mathematics, pages 1-14. American Mathematical Society, 1970.

[Law71]
Bill Lawvere. Quantifiers and sheaves. In Actes du Congrès International des Mathématiciens, volume 1, pages 329-334. Gauthier-Villars, 1971.

[Law72]
Bill Lawvere, editor. Toposes, Algebraic Geometry, and Logic, number 274 in Lecture Notes in Mathematics. Springer-Verlag, 1972.

[Law73]
Bill Lawvere. Metric spaces, generalised logic, and closed categories. In Rendiconti del Seminario Matematico e Fisico di Milano, volume 43. Tipografia Fusi, Pavia, 1973.

[LMW75]
Bill Lawvere, Christian Maurer, and Gavin Wraith, editors. Model Theory and Topoi, number 445 in Lecture Notes in Mathematics. Springer-Verlag, 1975.

[LS97]
Bill Lawvere and Stephen Schanuel. Conceptual Mathematics: a First Introduction to Categories. Cambridge University Press, 1997.

[LS81]
Daniel Lehmann and Michael Smyth. Algebraic specifications of data types: a synthetic approach. Mathematical Systems Theory, 14:97-139, 1981.

[Lei90]
Daniel Leivant. Contracting proofs to programs. In Odifreddi [Odi90], pages 279-327.

[Lew18]
Clarence Lewis. A Survey of Symbolic Logic. University of California Press, 1918. Republished by Dover, 1960.

[Lin71]
Carl Linderholm. Mathematics made Difficult. Wolfe, London, 1971.

[Lin69]
Fred Linton. An outline of functorial semantics. In Eckmann [Eck69], pages 7-52.

[Luk51]
Jan Lukasiewicz. Aristotle's Syllogistic from the Standpoint of Modern Formal Logic. Oxford University Press, 1951. Second edition, 1963.

[Luk63]
Jan Lukasiewicz. Elements of Mathematical Logic. Pergamon Press, 1963. Translated from Polish by Olgierd Wojtasiewicz.

[Luk70]
Jan Lukasiewicz. Selected Works. Studies in Logic and the Foundations of Mathematics. North-Holland, 1970. Edited by Ludwig Berkowski.

[Luo92]
Zhaohui Luo. A unifying theory of dependent types: the schematic approach. In Anil Nerode and Mikhail Taitslin, editors, Logical Foundations of Computer Science (Logic at Tver '92), number 620 in Lecture Notes in Computer Science, pages 293-304. Springer- Verlag, 1992.

[MW91]
Malcolm MacCallum and Francis Wright. Algebraic Computing with REDUCE: lecture notes from the First Brazilian School on Computer Algebra. Oxford University Press, 1991.

[MLB67]
Saunders Mac Lane and Garrett Birkhoff. Algebra. MacMillan, New York, 1967. Second edition, 1979.

[ML71]
Saunders Mac Lane. Categories for the Working Mathematician . Number 5 in Graduate Texts in Mathematics. Springer-Verlag, 1971.

[ML81]
Saunders Mac Lane. Mathematical models: a sketch for the philosophy of mathematics. American Mathematical Monthly, 88:462-472, 1981.

[ML79]
Saunders Mac Lane. Selected Papers. Springer- Verlag, 1979. Edited by Irving Kaplansky.

[ML86]
Saunders Mac Lane. Mathematics, Form and Function. Springer-Verlag, 1986.

[ML88]
Saunders Mac Lane. Categories and concepts in perspective. In Peter Duren, Richard Askey, and Uta Merzbach, editors, A Century of Mathematics in America, volume 1, pages 323-365. American Mathematical Society, 1988. Addendum in volume 3, pages 439-441.

[MLM92]
Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic: a First Introduction to Topos Theory. Universitext. Springer-Verlag, 1992.

[MR77]
Michael Makkai and Gonzalo Reyes. First Order Categorical Logic: Model-Theoretical Methods in the Theory of Topoi and Related Categories. Number 611 in Lecture Notes in Mathematics. Springer-Verlag, 1977.

[Mak87]
Michael Makkai. Stone duality for first order logic. Advances in Mathematics, 65:97-170, 1987.

[MP87]
Michael Makkai and Andrew Pitts. Some results on locally finitely presentable categories. Transactions of the American Mathematical Society, 299:473-496, 1987.

[MP90]
Michael Makkai and Robert Paré. Accessible Categories: the Foundations of Categorical Model Theory. Number 104 in Contemporary Mathematics. American Mathematical Society, 1990.

[Mak93]
Michael Makkai. The fibrational formulation of intuitionistic predicate logic. Notre Dame Journal of Formal Logic, 34:334-7 and 471-498, 1993.

[Mak96]
Michael Makkai. Avoiding the axiom of choice in category theory. Journal of Pure and Applied Algebra, 108:109-173, 1996.

[Mak97]
Michael Makkai. First order logic with dependent sorts. ftp.math.mcgill.ca, 1997.

[Mal71]
Anatolii Mal'cev. The Metamathematics of Algebraic Systems. Collected Papers 1936-67. Number 66 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1971. Edited by Benjamin Wells.

[Man98]
Paolo Mancosu. From Brouwer to Hilbert: the Debate on the Foundations of Mathematics in the 1920s. Oxford University Press, 1998.

[Man76]
Ernest Manes. Algebraic Theories. Number 26 in Graduate Texts in Mathematics. Springer-Verlag, 1976.

[Mar98]
Francisco Marmolejo. Continuous families of coalgebras. Journal of Pure and Applied Algebra, 130:197-215, 1998,

[ML75]
Per Martin-Löf. An intuitionistic theory of types: Predicative part. In Harvey Rose and John Sheperdson, editors, Logic Colloquium '73, number 80 in Studies in Logic and the Foundations of Mathematics, pages 73-118. North-Holland, 1975.

[ML84]
Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Naples, 1984.

[MR73]
Adrian Mathias and Hartley Rogers, editors. Cambridge Summer School in Mathematical Logic. Number 337 in Lecture Notes in Mathematics. Springer-Verlag, 1973.

[McC67]
Storrs McCall. Polish Logic, 1920-1939. Oxford University Press, 1967.

[MF87]
Ralph McKenzie and Ralph Freese. Commutator Theory for Congruence Modular Varieties. Number 125 in London Mathematical Society Lecture Notes. Cambridge University Press, 1987.

[MMT87]
Ralph McKenzie, George McNulty, and Walter Taylor. Algebras, Lattices, Varieties. Wadsworth and Brooks, 1987.

[McL92]
Colin McLarty. Elementary Categories, Elementary Toposes. Number 21 in Logic Guides. Oxford University Press, 1992.

[MNPS91]
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125-137, 1991.

[Mit65]
Barry Mitchell. Theory of Categories. Number 17 in Pure and applied mathematics. Academic Press, 1965.

[MS93]
John Mitchell and Andre Scedrov. Notes on sconing and relators. In Egon Börger, Gerhard Jäger, Hans Büning, and Michael Richter, editors, Computer Science Logic '92, number 702 in Lecture Notes in Computer Science, pages 352-378. Springer-Verlag, 1993.

[Mit96]
John Mitchell. Foundations for Programming Languages. MIT Press, 1996.

[Mog91]
Eugenio Moggi. Notions of computation and monads. Information and Computation, 93:55-92, 1991.

[Mon66]
Richard Montague. Fraenkel's addition to the axioms of Zermelo. In Bar-Hillel et al. [ BHPRR66], pages 91-114.

[Moo82]
Gregory Moore. Zermelo's Axiom of Choice: its Origins, Development, and Influence. Number 8 in Studies in the History of Mathematics and Physical Science. Springer-Verlag, 1982.

[MS55]
John Myhill and John Shepherson. Effective operations on partial recursive functions. Zeitschrift für Mathematische Logik und Gründlagen der Mathematik, pages 310-317, 1955.

[NST93]
Peter Neumann, Gabrielle Stoy, and Edward Thompson. Groups and Geometry. Oxford University Press, 1993.

[Nie82]
Susan Niefield. Cartesianness: Topological spaces, uniform spaces and affine varieties. Journal of Pure and Applied Algebra, 23:147-167, 1982.

[Noe83]
Emmy Noether. Gesammelte Abhandlungen. Springer-Verlag, 1983. Edited by Nathan Jabobson.

[NPS90]
Bengt Nordström, Kent Petersson, and Jan Smith. Programming in Martin-Löf's Type Theory: an Introduction. Number 7 in International Series of Monographs on Computer Science. Oxford University Press, 1990.

[Obt89]
Adam Obtulowicz. Categorical and algebraic aspects of Martin-Löf type theory. Studia Logica, 48:299-318, 1989.

[Odi89]
Piergiorgio Odifreddi. Classical Recursion Theory: the Theory of Functions and Sets of Natural Numbers. Number 125 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1989.

[Odi90]
Piergiorgio Odifreddi, editor. Logic and Computer Science. Number 31 in APIC Studies in Data Processing. Academic Press, 1990.

[Osi74]
Gerhard Osius. Categorical set theory: a characterisation of the category of sets. Journal of Pure and Applied Algebra, 4:79-119, 1974.

[Par76]
David Park. The Y-combinator in Scott's lambda-calculus models. Research Report CS-RR-013, Department of Computer Science, University of Warwick, June 1976. Revised, 1978.

[Pas65]
Boris Pasynkov. Partial topological products. Transactions of the Moscow Mathematical Society, 13:153-271, 1965.

[Pau87]
Lawrence Paulson. Logic and Computation: Interactive proof with Cambridge LCF. Number 2 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1987.

[Pau91]
Lawrence Paulson. ML for the Working Programmer. Cambridge University Press, 1991. Second edition, 1996.

[Pau92]
Lawrence Paulson. Designing a theorem prover. In Samson Abramsky et al., editors, Handbook of Logic in Computer Science, pages 415-475. Oxford University Press, 1992.

[Pau94]
Lawrence Paulson. Isabelle: a Generic Theorem Prover. Number 828 in Lecture Notes in Computer Science. Springer-Verlag, 1994.

[Pav90]
Du sko Pavlovi\'c. Predicates and Fibrations. PhD thesis, Rijksuniversiteit Utrecht, 1990.

[Pav91]
Du sko Pavlovi\'c. Constructions and predicates. In Pitt et al. [PCA+91 ], pages 173-197.

[Pea89]
Giuseppe Peano. Arithmetices Principia, Nova Methodo Exposita. Fratres Bocca, Turin, 1889. English translation, ``The Principles of Arithmetic, presented by a new method,'' in [vH67], pages 20-55.

[Pea73]
Giuseppe Peano. Selected Works of Giuseppe Peano. Toronto University Press, 1973. Translated and edited by Hubert Kennedy.

[Pei33]
Charles Sanders Peirce. Collected Papers. Harvard University Press, 1933. Edited by Charles Hartshorne and Paul Weiss.

[Pie91]
Benjamin Pierce. Basic Category Theory for Computer Scientists. Foundations of Computing. MIT Press, 1991.

[PRD +89]
David Pitt, David Rydeheard, Peter Dybjer, Andrew Pitts, and Axel Poigné, editors. Category Theory in Computer Science III, number 389 in Lecture Notes in Computer Science. Springer-Verlag, 1989.

[PCA +91]
David Pitt, Pierre-Louis Curien, Samson Abramsky, Andrew Pitts, Axel Poigné, and David Rydeheard, editors. Category Theory in Computer Science IV, number 530 in Lecture Notes in Computer Science. Springer-Verlag, 1991.

[Pit89]
Andrew Pitts. Non-trivial power types can't be subtypes of polymorphic types. In Logic in Computer Science IV, pages 6-13. IEEE Computer Society Press, 1989.

[PT89]
Andrew Pitts and Paul Taylor. A note on Russell's Paradox in locally cartesian closed categories. Studia Logica, 48:377-387, 1989.

[Pit95]
Andrew Pitts. Categorical logic. Technical Report 367, University of Cambridge Computer Laboratory, May 1995.

[PD97]
Andrew Pitts and Peter Dybjer, editors. Semantics and Logics of Computation, Publications of the Newton Institute. Cambridge University Press, 1997.

[Plo77]
Gordon Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223-255, 1977.

[Plo81]
Gordon Plotkin. Domain theory. Post-graduate lecture notes, known as the Pisa Notes; ftp.lfcs.ed.ac.uk, 1981.

[Poh89]
Wolfram Pohlers. Proof Theory: an Introduction. Number 1407 in Lecture Notes in Mathematics. Springer-Verlag, 1989.

[Pol45]
George Polya. How to Solve It: a New Aspect of Mathematical Method. Princeton University Press, 1945. Re- published by Penguin, 1990.

[Pra65]
Dag Prawitz. Natural Deduction: a Proof-Theoretical Study. Number 3 in Stockholm Studies in Philosophy. Almquist and Wiskell, 1965.

[Pra77]
Dag Prawitz. Meanings and proofs: on the conflict between classical and intutitionistic logic. Theoria, 43:2-40, 1977.

[Qui60]
Willard van Orman Quine. Word and Object. Studies in Communication. MIT Press, 1960.

[Ram31]
Frank Ramsey. Foundations of Mathematics. Kegan Paul, 1931.

[RS63]
Helena Rasiowa and Roman Sikorski. The Mathematics of Metamathematics. Number 41 in Monogrfie Matematyczne. Polish Scientific Publishers, 1963.

[Ras74]
Helena Rasiowa. An Algebraic Approach to Non-classical Logics. Number 78 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1974.

[Rey83]
John Reynolds. Types, abstraction and parametric polymorphism. In Richard Mason, editor, Information Processing, pages 513-524. North-Holland, 1983.

[Rey84]
John Reynolds. Polymorhism is not set-theoretic. In Gilles Kahn, David MacQueen, and Gordon Plotkin, editors, Semantics of Data Types, number 173 in Lecture Notes in Computer Science, pages 145-156. Springer-Verlag, 1984.

[RP93]
John Reynolds and Gordon Plotkin. On functors expressible in the polymorphic lambda calculus. Information and Computation, 105:1-29, 1993.

[Rey98]
John Reynolds. Theories of Programming Languages. Cambridge University Press, 1998.

[Ric56]
Gordon Rice. Recursive and recursively enumerable orders. Transactions of the American Mathematical Society, 83:277, 1956.

[Rob66]
Abraham Robinson. Non-standard Analysis. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1966.

[Rob82]
Derek Robinson. A Course in the Theory of Groups. Number 80 in Graduate Texts in Mathematics. Springer-Verlag, 1982. Second edition, 1996.

[RR88]
Edmund Robinson and Giuseppe Rosolini. Categories of partial maps. Information and Computation, 79:95-130, 1988.

[Rus03]
Bertrand Russell. The Principles of Mathematics. Cambridge University Press, 1903.

[Rus08]
Bertrand Russell. Mathematical logic based on the theory of types. American Journal of Mathematics, 30:222-262, 1908. Reprinted in [vH67], pages 150-182.

[RW13]
Bertrand Russell and Alfred North Whitehead. Principia Mathematica. Cambridge University Press, 1910-13.

[RB88]
David Rydeheard and Rod Burstall. Computational Category Theory. Prentice-Hall, 1988.

[Sam48]
Pierre Samuel. On universal mappings and free topological groups. Bulletin of the American Mathematical Society, 54:591-598, 1948.

[SS82]
Andre Scedrov and Philip Scott. A note on the Friedman slash and Freyd covers. In Troelstra and van Dalen [ TvD82], pages 443-452.

[Sch93]
Andrea Schalk. Domains arising as algebras for power space constructions. Journal of Pure and Applied Algebra, 1993.

[Sch67]
Joseph Schoenfield. Mathematical Logic. Addison -Wesley, 1967.

[Sco66]
Dana Scott. More on the axiom of extensionality. In Bar-Hillel et al. [BHPRR66], pages 115-139.

[Sco70a]
Dana Scott. Constructive validity. In Michel Laudet, D. Lacombe, L. Nolin, and M. Schützenberger, editors, Automatic Demonstration, number 125 in Lecture Notes in Mathematics, pages 237-275. Springer-Verlag, 1970.

[Sco70b]
Dana Scott. Outline of a mathematical theory of computation. In Information Sciences and Systems, pages 169-176. Princeton University Press, 1970.

[Sco76]
Dana Scott. Data types as lattices. SIAM Journal on Computing, 5:522-587, 1976.

[Sco79]
Dana Scott. Identity and existence in intuitionistic logic. In Fourman et al. [FMS79], pages 660-696.

[SS70]
J. Arthur Seebach and Lynn Arthur Steen. Counterexamples in Topology. Holt, Rinehart and Winston, 1970. Republished by Springer-Verlag, 1978 and by Dover, 1995.

[See84]
Robert Seely. Locally cartesian closed categories and type theory. Mathematical Proceedings of the Cambridge Philosophical Society, 95:33-48, 1984.

[See87]
Robert Seely. Categorical semantics for higher order polymorphic lambda calclus. Journal of Symbolic Logic, 52:969-989, 1987.

[See89]
Robert Seely. Linear logic, *-autonomous categories and cofree algebras. In Gray and Scedrov [ GS89], pages 371-382.

[Ser71]
Jean-Pierre Serre. Repésentations Linéaires des Groupes Finis. Hermann, 1971. English translation, ``Linear representations of finite groups'' by Leonard Scott, Springer-Verlag, Graduate Texts in Mathematics 42, 1976, reprinted 1986.

[Sha91]
Stewart Shapiro. Foundations without Foundationalism: a Case for Second-order Logic. Number 17 in Logic Guides. Oxford University Press, 1991.

[Sko22]
Thoralf Skolem. Einige Bemerkungen zur axiomatischen Begründung der Mengenlehre. In Skandinaviska matematikenkongressen, pages 217-232. Akademiska Bokhandeln, 1922. English translation, ``Some Remarks on Axiomatized Set Theory'' in [vH67], pages 290-301.

[Sko70]
Thoralf Skolem. Selected Works in Logic. Universitetsforlaget, Oslo, 1970. Edited by Jens Erik Fenstad.

[Ste67]
Norman Steenrod. A convenient category of topological spaces. Michigan Mathematics Journal, 14:133-152, 1967.

[Sto37]
Marshall Stone. Applications of the theory of Boolean rings to general topology. Transactions of the American Mathematical Society, 41:375-481, 1937.

[SW73]
Ross Street and Robert Walters. The comprehensive factorization of a functor. Bulletin of the American Mathematical Society, 79:936-941, 1973.

[Str80]
Ross Street. Cosmoi of internal categories. Transactions of the American Mathematical Society, 258:271-318, 1980.

[Str91]
Thomas Streicher. Semantics of Type Theory: Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions . Progress in Theoretical Computer Science. Birkhäuser, 1991. His 1988 Passau Ph.D. thesis.

[Str69]
Dirk Struik. A Source Book in Mathematics, 1200-1800. Harvard University Press, 1969.

[Sty69]
N. I. Styazhkin. History of Mathematical Logic from Leibniz to Peano. MIT Press, 1969. Translated from Russian, originally published by Nauka, Moscow, 1964.

[Tai75]
William Tait. A realizability interpretation of the theory of species. In R. Parik, editor, Logic Colloquium, pages 240-251. Springer-Verlag, 1975.

[Tak75]
Gaisi Takeuti. Proof Theory. Number 81 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1975. Second edition, 1987.

[Tar56]
Alfred Tarski. Logic, Semantics, Metamathematics. Oxford University Press, 1956. Edited by J. H. Woodger.

[Tay86a]
Paul Taylor. Internal completeness of categories of domains. In David Pitt, editor, Category Theory and Computer Programming, number 240 in Lecture Notes in Computer Science, pages 449-465. Springer-Verlag, 1986.

[Tay86b]
Paul Taylor. Recursive Domains, Indexed Category Theory and Polymorphism. PhD thesis, Cambridge University, 1986.

[Tay87]
Paul Taylor. Homomorphisms, bilimits and saturated domains - some very basic domain theory. ftp.dcs.qmw.ac.uk, 1987.

[Tay88]
Paul Taylor. The trace factorisation of stable functors. 1988.

[Tay89]
Paul Taylor. Quantitative domains, groupoids and linear logic. In Pitt et al. [ PRD+89], pages 155-181.

[Tay90]
Paul Taylor. An algebraic approach to stable domains. Journal of Pure and Applied Algebra, 64:171-203, 1990.

[Tay91]
Paul Taylor. The fixed point property in synthetic domain theory. In Gilles Kahn, editor, Logic in Computer Science 6, pages 152-160. IEEE Computer Society Press, 1991.

[Tay96a]
Paul Taylor. Intuitionistic sets and ordinals. Journal of Symbolic Logic, 61:705-744, 1996.

[Tay96b]
Paul Taylor. On the general recursion theorem. 1996.

[Tay98]
Paul Taylor. An abstract stone duality, I: Geometric and higher order logic. 1998. In preparation.

[Ten81]
Robert Tennent. Principles of Programming Languages. Prentice-Hall, 1981.

[Ten91]
Robert Tennent. Semantics of Programming Languages. International Series in Computer Science. Prentice-Hall, 1991.

[Tie72]
Miles Tierney. Sheaf theory and the continuum hypothesis. In Lawvere [Law72], pages 13-42.

[Tro69]
Anne Sjerp Troelstra. Principles of Intuitionism. Number 95 in Lecture Notes in Mathematics. Springer-Verlag, 1969.

[Tro77]
Anne Sjerp Troelstra. Choice Sequences: a Chapter of Inttuitionistic Mathematics. Logic Guides. Oxford University Press, 1977.

[TvD82]
Anne Sjerp Troelstra and Dirk van Dalen, editors. L. E. J.  Brouwer Centenary Symposium, number 110 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1982.

[TvD88]
Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in Mathematics, an Introduction. Number 121 and 123 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1988.

[TS96]
Anne Sjerp Troelstra and Helmut Schwichtenberg. Basic Proof Theory. Number 43 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1996.

[Tur35]
Alan Turing. On computable numbers with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society (2), 42:230-265, 1935.

[vD80]
Dirk van Dalen. Logic and Structure. Universitext . Springer-Verlag, 1980. Second edition, 1983.

[vdW31]
Bartel van der Waerden. Moderne Algebra. Ungar, 1931. Fifth edition, Springer-Verlag, 1960; English translation by Fred Blum and John Schulenberger, ``Algebra,'' Springer-Verlag, 1971.

[vH67]
Jan van Heijenoort, editor. From Frege to Gödel: a Source Book in Mathematical Logic, 1879-1931. Harvard University Press, 1967. Reprinted 1971, 1976.

[Vic88]
Steven Vickers. Topology via Logic. Number 5 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1988.

[vN61]
John von Neumann. Collected Works. Pergamon Press, 1961. Edited by A. H. Taub.

[Web80]
Judson Chambers Webb. Mechanism, Mentalism and Metamathematics: an Essay on Finitism. Number 137 in Synthese Library. Reidel, 1980.

[Wel96]
Charles Wells. The Handbook of Mathematical Discourse, http://www-math.cwru.edu/ ~ cfw2/abouthbk.htm

[Wey19]
Hermann Weyl. Der Circulus vitiosus in der heutigen Begrü ndung der Analysis. Jahrbericht der deutschen M atematiker-Vereinigung, 28:85-92, 1919. English translation, ``The Continuum: a Critical Examination of the Foundations of Analysis'' by Stephen Pollard and Thomas Bole, published by Thomas Jefferson University Press, 1987, reprinted by Dover, 1993.

[Wey68]
Hermann Weyl. Gesammelte Abhandlungen. Springer-Verlag, 1968. Edited by K. Chandrasekharan.

[ZS58]
Oscar Zariski and Pierre Samuel. Commutative Algebra. Van Nostrand, 1958. Reprinted by Springer-Verlag, Graduate Texts in Mathematics, numbers 28-9, 1975.

[Zer08a]
Ernst Zermelo. Neuer Beweis für die Möglichkeit einer Wohlordnung. Mathematische Annalen, 65:107-128, 1908. English translation, ``New proof that every set can be well ordered'' in [vH67], pages 183-198.

[Zer08b]
Ernst Zermelo. Untersuchungen über die Grundlagen der Mengenlehre I. Mathematische Annalen, 65:261- 281, 1908. English translation, ``Investigations in the foundations of set theory'' in [vH67], pages 199-215.