% =========================================================================

%    Bibliography for ``Practical Foundations of Mathematics''
%    Paul Taylor    pt(at)dcs.qmw.ac.uk

%    Cambridge University Press 1998,  ISBN 0-521-63107-6
%    Cambridge Studies in Advanced Mathematics 59		  
%    http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/
		  
% =========================================================================
%  Run this through LaTeX, then BibTeX, then LaTeX and LaTeX again:
		  
%  latex prafm-ref.bib;
%  bibtex prafm-ref;
%  latex prafm-ref.bib;
%  latex prafm-ref.bib;
%  xdvi prafm-ref.dvi	  
		  
\documentclass{article}
\title{Bibliography for\\
Practical Foundations of Mathematics}
\author{Paul Taylor\\
\texttt{pt\char64 dcs.qmw.ac.uk}\\
\texttt{http://www.dcs.qmw.ac.uk/$\sim$pt/Practical\_Foundations/}\\
Cambridge University Press\\
Cambridge Studies in Advanced Mathematics, 59\\
ISBN 0 521 63107 6}	
\date{1988}	  
\usepackage{a4wide}% leave this out if you don't have it
\def\naive{na\"\i ve }
\def\Naive{Na\"\i ve }
\def\tuck{}
\begin{document}
\maketitle	  
\nocite{*}
\bibliographystyle{alpha-unsrt}
\bibliography{prafm-ref}
\end{document}
\endinput
		  
% =========================================================================

@incollection{JungA:domt,
 author		= {Abramsky, Samson and Jung, Achim},
 title		= {Domain Theory},
 editor		= {Abramsky, Samson and others},
 booktitle	= {Handbook of Logic in Computer Science},
 publisher	= {Oxford University Press},
 volume		= 3,
 year		= 1994,
 pages		= {1--168}}


@book{AczelP:nonwfs,
 author		= {Aczel, Peter},
 title		= {Non-well-founded Sets},
 publisher	= {Center for the Study of Language and Information,
	Stanford University},
 series		= {Lecture Notes},
 number		= 14,
 year		= 1988,
 isbn		= {511.322 3 / 0937073229}}


@book{AdamekJ:locpac,
 author		= {Ad{\'a}mek, Ji{\v r}i and Rosick{\'y}, Ji{\v r}i},
 title		= {Locally Presentable and Accessible Categories},
 publisher	= {Cambridge University Press},
 series		= {London Mathematical Society Lecture Notes},
 number		= 189,
 year		= 1994,
 isbn		= {0-521-42261-2}}


@article{AgeronP:logs,
 author		= {Ageron, Pierre},
 title		= {The Logic of Structures},
 journal	= {Journal of Pure and Applied Algebra},
 volume		= 79,
 year		= 1992,
 pages		= {15--34}}


@inproceedings{StreicherT:catrrf,
 author		= {Altenkirch, Thorsten and Hofmann, Martin and Streicher, Thomas},
 title		= {Categorical Reconstruction of
	a Reduction-Free Normalisation Proof},
 editor		= {Johnstone, Peter and Pitt, David and Rydeheard, David},
 booktitle	= {Category Theory and Computer Science {VI}},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Computer Science},
 number		= 953,
 year		= 1995,
 pages		= {182--199},
 isbn		= 3540601643}


@book{AmadioRW:domlc,
 author		= {Amadio, Roberto and Curien, Pierre-Louis},
 title		= {Domains and Lambda-Calculi},
 publisher	= {Cambridge University Press},
 series		= {Cambridge Tracts in Theoretical Computer Science},
 number		= 46,
 year		= 1998,
 isbn		= {0 521 62277 8}}


@book{AppelAW:comwc,
 author		= {Appel, Andrew},
 title		= {Compiling with Continuations},
 publisher	= {Cambridge University Press},
 year		= 1992,
 pages		= {205--214},
 isbn		= {005.453 13 / 0521416957}}


@proceedings{GrothendieckA:semga4,
 title		= {S{\'e}minaire de G{\'e}ometrie Alg{\'e}brique,~{IV}:
	Th\'eorie des Topos},
 editor		= {Artin, Michael and Grothendieck, Alexander and Verdier, Jean-Louis},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= {269--270},
 year		= 1964,
 note		= {Second edition, 1972},
 review		= {MR 50/7130--1}}


@inproceedings{BaezJC:intnc,
 author		= {Baez, John},
 title		= {An Introduction to $n$-Categories},
 editor		= {Moggi, Eugenio and Rosolini, Giuseppe},
 booktitle	= {Category Theory and Computer Science~{VII}},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Computer Science},
 number		= 1290,
 year		= 1997,
 pages		= {1--33}}


@book{BarendregtHP:lamcss,
 author		= {Barendregt, Henk},
 title		= {The Lambda Calculus: its Syntax and Semantics},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 number		= 103,
 year		= 1981,
 note		= {Second edition, 1984},
 isbn		= {0-444-87508-5}}


@incollection{BarendregtHP:lamct,
 author		= {Barendregt, Henk},
 title		= {Lambda Calculi with Types},
 editor		= {Abramsky, Samson and others},
 booktitle	= {Handbook of Logic in Computer Science},
 publisher	= {Oxford University Press},
 volume		= 2,
 year		= 1992,
 pages		= {117--309},
 isbn		= 0198537611}


@proceedings{BarHillelY:essfm,
 title		= {Essays of the Foundations of Mathematics},
 editor		= {Bar-Hillel, Yehoshua and Poznanski, E. I. J. and Rabin, M. O. and Robinson, Abraham},
 booktitle	= {Essays on the Foundations of Mathematics},
 publisher	= {Magnes Press, Hebrew University},
 year		= 1966,
 note		= {Distributed by Oxford University Press}}


@inproceedings{BeckJ:LNM80,
 author		= {Barr, Michael and Beck, Jon},
 title		= {Homology and Standard Constructions},
 pages		= {245--335},
 crossref	= {EckmannB:semtch}}


@book{BarrM:exaccs,
 title		= {Exact Categories and Categories of Sheaves},
 editor		= {Barr, Michael and Grillet, Pierre and van Osdol, Donovan},
 booktitle	= {Exact Categories and Categories of Sheaves},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 236,
 year		= 1971,
 isbn		= 3540056785}


@book{BarrM:staac,
 author		= {Barr, Michael},
 title		= {{$*$}-Autonomous Categories},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 752,
 year		= 1979}


@book{BarrM:toptt,
 author		= {Barr, Michael and Wells, Charles},
 title		= {Toposes, Triples, and Theories},
 publisher	= {Springer-Verlag},
 series		= {Grundlehren der mathematischen {W}issenschaften},
 number		= 278,
 year		= 1985,
 isbn		= {0-387-96115-1 and 3-540-96115-1},
 callno		= {512.86 B26t},
 lccn		= {QA169 .B346 1985}}


@book{BarrM:cattcs,
 author		= {Barr, Michael and Wells, Charles},
 title		= {Category Theory for Computing Science},
 publisher	= {Prentice-Hall},
 series		= {International Series in Computer Science},
 year		= 1990,
 note		= {Second edition, 1995},
 isbn		= {0-13-120486-6},
 lccn		= {QA76.9.M35B37 1990}}


@article{BarrM:autcll,
 author		= {Barr, Michael},
 title		= {{$*$}-{A}utonomous Categories and Linear Logic},
 journal	= {Mathematical Structures in Computer Science},
 volume		= 1,
 year		= 1991,
 pages		= {159--178}}


@book{BarwiseJ:hanml,
 title		= {Handbook of Mathematical Logic},
 editor		= {Barwise, Jon},
 booktitle	= {Handbook of Mathematical Logic},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 number		= 90,
 year		= 1977,
 isbn		= {0 444 863888 5},
 lib_congress	= {QA9.H32 511'.3 76-26032}}


@book{BeesonMJ:foucm,
 author		= {Beeson, Michael},
 title		= {Foundations of Constructive Mathematics:
	Metamathematical Studies},
 publisher	= {Springer-Verlag},
 series		= {Ergebnisse der Mathematik und ihrer Grenzgebiete},
 number		= 6,
 year		= 1980,
 note		= {Second edition, 1985},
 isbn		= 0387121730}


@book{BellJL:toplst,
 author		= {Bell, John Lane},
 title		= {Toposes and Local Set Theories: an Introduction},
 publisher	= {Oxford University Press},
 series		= {Logic Guides},
 number		= 14,
 year		= 1988}


@article{BenabouJ:fibcfn,
 author		= {B{\'e}nabou, Jean},
 title		= {Fibred Categories and the Foundations of
	\Naive Category Theory},
 journal	= {Journal of Symbolic Logic},
 volume		= 50,
 year		= 1985,
 pages		= {10--37}}


@book{BenacerrafP:phimsr,
 title		= {Philosophy of Mathematics: Selected Readings},
 editor		= {Benacerraf, Paul and Putnam, Hilary},
 booktitle	= {Philosophy of Mathematics: Selected Readings},
 publisher	= {Prentice-Hall},
 year		= 1964,
 note		= {Second edition, Cambridge University Press, 1983},
 isbn		= {0 521 22796 8}}


@incollection{BenacerrafP:whancn,
 author		= {Benacerraf, Paul},
 title		= {What Numbers could not be},
 pages		= {272--294},
 crossref	= {BenacerrafP:phimsr}}


@article{BernaysP:plam,
 author		= {Bernays, Paul},
 title		= {Sur le Platonisme dans les Math\'ematiques},
 journal	= {Enseignement Math\'ematique},
 volume		= 34,
 year		= 1935,
 pages		= {52--69},
 note		= {English translation, ``Platonism in Mathematics''
	in \cite{BenacerrafP:phimsr}, pages 258--271}}


@book{BibelW:auttp,
 author		= {Bibel, Wolfgang},
 title		= {Automated Theorem Proving},
 publisher	= {Friedrich Vieweg \& Sohn},
 address	= {Braunschweig},
 year		= 1982,
 note		= {Second edition, 1987}}


@book{BirkhoffG:surma,
 author		= {Birkhoff, Garrett and Mac Lane, Saunders},
 title		= {A Survey of Modern Algebra},
 publisher	= {MacMillan},
 address	= {New York},
 year		= 1941,
 note		= {Fourth edition, 1977},
 isbn		= 0023100702}


@inproceedings{BirkhoffG:risma,
 author		= {Birkhoff, Garrett},
 title		= {The Rise of Modern Algebra},
 booktitle	= {Men and Institutions in {A}merican Mathematics},
 editor		= {Tarwater, Jan Dalton and White, John and Miller, John},
 publisher	= {Texas Technical University},
 year		= 1976,
 pages		= {41--86},
 brit_lib	= {YA.1987.b.5020}}


@book{BishopE:cona,
 author		= {Bishop, Errett and Bridges, Douglas},
 title		= {Constructive Analysis},
 publisher	= {Springer-Verlag},
 series		= {Grundlehren der mathematischen {W}issenschaften},
 number		= 279,
 year		= 1985,
 isbn		= 3540150668}


@book{BlackM:natm,
 author		= {Black, Max},
 title		= {The Nature of Mathematics, a Critical Survey},
 publisher	= {Kegan Paul},
 series		= {International Library of Psychology},
 year		= 1933}


@book{BochenskiI:ancfl,
 author		= {Bochenski, Josef},
 title		= {Ancient Formal Logic},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 year		= 1951}


@book{BoehnerP:medlod,
 author		= {Boehner, Philotheus},
 title		= {Medieval Logic: an Outline of its Development from 1250 to c.1400},
 publisher	= {Manchester University Press},
 year		= 1952}


@book{BoehnerP:colao,
 author		= {Boehner, Philotheus},
 title		= {Collected articles on {O}ckham},
 publisher	= {Franciscan Institute},
 year		= 1958,
 note		= {Edited by Elio Marie Buytaert}}


@book{BolzanoB:pare,
 author		= {Bolzano, Bernard},
 title		= {Paradoxien des {U}ndlichen},
 year		= 1851,
 note		= {English translation, ``Paradoxes of the Infinite'' by
	Fr. Prihonsky, published by Routledge, 1950}}


@book{BoolosGS:coml,
 author		= {Boolos, George and Jeffrey, Richard},
 title		= {Computability and Logic},
 publisher	= {Cambridge University Press},
 year		= 1974,
 note		= {Third edition, 1989},
 isbn		= {052120402X}}


@book{BoolosG:logp,
 author		= {Boolos, George},
 title		= {The Logic of Provability},
 publisher	= {Cambridge University Press},
 year		= 1993,
 lccn		= {BC199.M6B65 92-43610},
 isbn		= 052143328}


@book{BoolosG:logll,
 author		= {Boolos, George},
 title		= {Logic, Logic and Logic},
 publisher	= {Harvard University Press},
 year		= 1998,
 note		= {Edited by Richard Jeffrey},
 isbn		= 0674537661}


@book{BorceuxF:hanca,
 author		= {Borceux, Francis},
 title		= {Handbook of Categorical Algebra},
 publisher	= {Cambridge University Press},
 series		= {Encyclopedia of Mathematics and its Applications},
 number		= 50,
 year		= 1994,
 note		= {Three volumes},
 isbn		= {0521441781 052144179X 0521441803}}


@book{BourbakiN:elemte,
 author		= {Bourbaki, Nicolas},
 title		= {El\'ements de Math\'ematique {XXII}:
	Th\'eories des Ensembles, Livre {I}, Structures},
 publisher	= {Hermann},
 series		= {Actualit\'es scientifiques et industrielles},
 number		= 1258,
 year		= 1957,
 note		= {English translation, ``Theory of Sets\tuck,'' 1968}}


@book{BoyerCB:hism,
 author		= {Boyer, Carl},
 title		= {A History of Mathematics},
 publisher	= {Wiley},
 year		= 1968,
 note		= {Revised edition by Uta Merzbach, Wiley, 1989},
 isbn		= 0471097632}


@book{BoyerRS:comlh,
 author		= {Boyer, Robert and Moore, J. Strother},
 title		= {A Computational Logic Handbook},
 publisher	= {Academic Press},
 series		= {Perspectives in Computing},
 number		= 23,
 year		= 1988,
 isbn		= 0121229521}


@book{BrouwerLEJ:colw,
 author		= {Brouwer, Jan},
 title		= {Collected Works: Philosophy and Foundations of Mathematics},
 booktitle	= {Collected Works},
 publisher	= {North-Holland},
 volume		= 1,
 year		= 1975,
 note		= {Edited by Arend Heyting},
 isbn		= 0444104747}


@book{BrouwerLEJ:brocli,
 author		= {Brouwer, Jan},
 title		= {Brouwer's {C}ambridge Lectures on Intuitionism},
 publisher	= {Cambridge University Press},
 year		= 1981,
 note		= {Edited by Dirk van Dalen}}


@proceedings{HilbertD:matpld,
 title		= {Mathematical Developments Arising from Hilbert Problems},
 editor		= {Browder, Felix},
 publisher	= {American Mathematical Society},
 series		= {Proceedings of Symposia in Pure Mathematics},
 number		= 28,
 year		= 1976}


@article{BrownR:grogbs,
 author		= {Brown, Ronald},
 title		= {From Groups to Groupoids: a Brief Survey},
 journal	= {Bulletin of the London Mathematical Society},
 volume		= 19,
 year		= 1987,
 pages		= {113--134}}


@book{BrownR:topgag,
 author		= {Brown, Ronald},
 title		= {Topology: a Geometric Account of General Topology,
	Homotopy Types and the Fundamental Groupoid},
 publisher	= {Ellis Horwood},
 series		= {Mathematics and its Applications},
 year		= 1988,
 note		= {First edition ``Elements of modern topology\tuck,'' 1968},
 isbn		= 0745802311}


@book{BurrisS:couua,
 author		= {Burris, Stanley and Sankappanavar, H. P.},
 title		= {A Course in Universal Algebra},
 publisher	= {Springer-Verlag},
 series		= {Graduate Texts in Mathematics},
 number		= 78,
 year		= 1981,
 isbn		= 0387905782}


@article{BurroniA:algg,
 author		= {Burroni, Albert},
 title		= {Alg{\`e}bres Graphiques},
 journal	= {Cahiers de Topologie et G{\'e}om{\'e}trie
	Diff{\'e}rentielle},
 volume		= {XXII},
 year		= 1981}


@book{CajoriF:hism,
 author		= {Cajori, Florian},
 title		= {A History of Mathematics},
 publisher	= {MacMillan},
 year		= 1893,
 note		= {Fifth edition, Chelsea, N.Y., 1991},
 isbn		= 0828423036,
 comment	= {1924; Macmillan, 1926.2nd ed., revised and enlarged.}}


@book{CajoriF:hismn,
 author		= {Cajori, Florian},
 title		= {A History of Mathematical Notations},
 publisher	= {Open Court},
 year		= 1928,
 note		= {Reprinted by Dover, 1993}}


@book{CameronPJ:inta,
 author		= {Cameron, Peter},
 title		= {Introduction to Algebra},
 publisher	= {Oxford University Press},
 year		= 1998,
 isbn		= 0198501943}


@book{CantorG:conftf,
 author		= {Cantor, Georg},
 title		= {Contributions to the Founding of the Theory of Transfinite Numbers},
 publisher	= {Open Court},
 year		= 1915,
 note		= {Translated and edited by Philip Jourdain; reprinted by Dover, 1955}}


@book{CantorG:gesamp,
 author		= {Cantor, Georg},
 title		= {Gesammelte {A}bhandlungen mathematischen und philosophischen {I}nhalts},
 publisher	= {Springer-Verlag},
 year		= 1932,
 note		= {Edited by Ernst Zermelo; reprinted by Olms, Hildeshaim, 1962}}


@proceedings{CarboniA:comctc,
 title		= {Proceedings of the 1990 Como Category Theory Conference},
 editor		= {Carboni, Aurelio and Peddicchio, Maria-Cristina and Rosolini, Giuseppe},
 booktitle	= {Proceedings 1990 Como Category Theory Conference},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 1488,
 year		= 1991}


@article{WaltersRFC:inteds,
 author		= {Carboni, Aurelio and Lack, Steve and Walters, Robert},
 title		= {Introduction to extensive and distributive categories},
 journal	= {Journal of Pure and Applied Algebra},
 volume		= 84,
 year		= 1993,
 pages		= {145--158}}


@book{CarnapR:logss,
 author		= {Carnap, Rudolf},
 title		= {Logische {S}yntax der {S}prache},
 address	= {Vienna},
 year		= 1934,
 note		= {English translation by Amethe Smeaton,
	``The Logical Syntax of Language\tuck,'' Kegan Paul, 1937}}


@book{CartanH:homa,
 author		= {Cartan, Henri and Eilenberg, Sammy},
 title		= {Homological Algebra},
 publisher	= {Princeton University Press},
 year		= 1956}


@article{CartmellJ:genatc,
 author		= {Cartmell, John},
 title		= {Generalised Algebraic Theories and Contextual Categories},
 journal	= {Annals of Pure and Applied Logic},
 volume		= 32,
 year		= 1986,
 pages		= {209--243},
 qmwlib		= {bay 177}}


@book{ChangCC:modt,
 author		= {Chang, Chen Chung and Keisler, Jerome},
 title		= {Model Theory},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 number		= 73,
 year		= 1973,
 note		= {Third edition, 1990},
 isbn		= {0720406927 0444880542}}


@book{ChapmanJ:relctg,
 author		= {Chapman, Jon and Rowbottom, Frederick},
 title		= {Relative Category Theory and Geometric Morphisms:
	a Logical Approach},
 publisher	= {Oxford University Press},
 series		= {Logic Guides},
 number		= 16,
 year		= 1992,
 isbn		= 0198534345}


@book{Church:intml,
 author		= {Church, Alonso},
 title		= {Introduction to Mathematical Logic},
 publisher	= {Princeton University Press},
 year		= 1956}


@article{CockettJRB:intdc,
 author		= {Cockett, Robin},
 title		= {Introduction to distributive categories},
 journal	= {Mathematical Structures in Computer Science},
 volume		= 3,
 year		= 1993,
 pages		= {277--307}}


@proceedings{CohenAM:somtca,
 title		= {Some Tapas of Computer Algebra},
 editor		= {Cohen, A. M. and Cuypers, H. and Sterk, H.},
 booktitle	= {Some Tapas of Computer Algebra},
 publisher	= {Springer-Verlag},
 series		= {Algorithms and Computation in Mathematics},
 number		= 4,
 year		= 1998,
 isbn		= {3-540-63480-0},
 keywords	= {Computer algebra;
	Symbolic Computation, Computer Algebra,
	Algebraic Manipulation;
	Written for students and researchers in mathematics
	and computer science}}


@book{CohenPJ:settch,
 author		= {Cohen, Paul},
 title		= {Set Theory and the Continuum Hypothesis},
 publisher	= {W.A.~Benjamin},
 year		= 1966,
 review		= {MR 38/999}}


@book{CohnPM:alg2,
 author		= {Cohn, Paul},
 title		= {Algebra},
 publisher	= {Wiley},
 volume		= 2,
 year		= 1977,
 isbn		= {0-471-01823-6},
 libcongress	= {73--2780}}


@book{CohnPM:unia,
 author		= {Cohn, Paul},
 title		= {Universal Algebra},
 publisher	= {Reidel},
 series		= {Mathematics and its Applications},
 number		= 6,
 year		= 1981,
 note		= {Originally published by Harper and Row, 1965},
 isbn		= {90-277-1213-1},
 libcong	= {80--29568}}


@book{ConwayJH:regafm,
 author		= {Conway, John Horton},
 title		= {Regular Algebra and Finite Machines},
 publisher	= {Chapman and Hall},
 year		= 1971,
 isbn		= 0412106205}


@book{ConwayJH:onng,
 author		= {Conway, John Horton},
 title		= {On Numbers and Games},
 publisher	= {Academic Press},
 series		= {London Mathematical Society Monographs},
 number		= 6,
 year		= 1976,
 isbn		= 0121863506}


@article{CoquandTFH:calc,
 author		= {Coquand, Thierry and Huet, G{\'e}rard},
 title		= {The Calculus of Constructions},
 journal	= {Information and Computation},
 volume		= 76,
 year		= 1988,
 pages		= {95--120}}


@incollection{CoquandTFH:meticc,
 author		= {Coquand, Thierry},
 title		= {Metamathematical Investigations of a Calculus of Constructions},
 pages		= {91--122},
 crossref	= {OdifreddiP:logcs}}


@incollection{CoquandTFH:anabpt,
 author		= {Coquand, Thierry},
 title		= {On the Analogy between Propositions and Types},
 editor		= {Huet, G{\'e}rard},
 booktitle	= {Logical Foundations of Functional Programming},
 publisher	= {Addison-Wesley},
 year		= 1990,
 pages		= {399--418},
 labels		= {anabpt}}


@inproceedings{CoquandTFH:comccl,
 author		= {Coquand, Thierry},
 title		= {Computational Content of Classical Logic},
 pages		= {33--78},
 crossref	= {PittsAM:semlc}}


@inproceedings{CosteM:locssp,
 author		= {Coste, Michel},
 title		= {Localisation, Spectra and Sheaf Representation},
 year		= 1979,
 pages		= {212--238},
 crossref	= {FourmanMP:apps}}


@book{CouturatL:primap,
 author		= {Couturat, Louis},
 title		= {Les Principes des Math\'ematiques,
	avec un Appendice sur le Philosophie de Kant},
 year		= 1905}


@article{CroleRL:newffcff,
 author		= {Crole, Roy and Pitts, Andrew},
 title		= {New Foundations for Fixpoint Computations:
	{FIX}-Hyperdoctrines and the {FIX}-Logic},
 journal	= {Information and Computation},
 volume		= 98,
 year		= 1992,
 pages		= {171--210}}


@book{CroleRL:catt,
 author		= {Crole, Roy},
 title		= {Categories for Types},
 publisher	= {Cambridge University Press},
 series		= {Cambridge Mathematical Textbooks},
 year		= 1993,
 isbn		= 0521450926}


@article{CubricD:norye,
 author		= {{\protect\v C}ubri{\'c}, Djordje and Dybjer, Peter and Scott, Philip},
 title		= {Normalisation and the {Y}oneda Embedding},
 journal	= {Mathematical Structures in Computer Science},
 volume		= 8,
 year		= 1998,
 pages		= {153--192}}


@book{CurienPL:catcsa,
 author		= {Curien, Pierre-Louis},
 title		= {Categorical Combinators, Sequential Algorithms, and Functional
	Programming},
 publisher	= {Pitman},
 series		= {Research Notes in Theoretical Computer Science},
 year		= 1986,
 note		= {Second edition, Birkh{\"a}user,
	Progress in Theoretical Computer Science,
	1993},
 isbn		= 0470202904}


@book{CurryHB:coml1,
 author		= {Curry, Haskell and Feys, Robert},
 title		= {Combinatory Logic {I}},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 year		= 1958,
 note		= {Volume II, with Jonathan Seldin, 1972}}


@book{CurryHB:fouml,
 author		= {Curry, Haskell},
 title		= {Foundations of Mathematical Logic},
 publisher	= {McGraw--Hill},
 year		= 1963,
 note		= {Republished by Dover, 1977}}


@proceedings{CurryHB:hbcecl,
 title		= {To H.B. Curry: Essays on Combinatory Logic,
	Lambda Calculus and Formalism},
 editor		= {Curry, Haskell and Seldin, Jonathan and Hindley, Roger},
 booktitle	= {To H.B. Curry: Essays on Combinatory Logic,
	Lambda Calculus and Formalism},
 publisher	= {Academic Press},
 year		= 1980,
 isbn		= 0123490502}


@book{DaubenJW:geocmp,
 author		= {Dauben, Joseph Warren},
 title		= {Georg {C}antor:
	his Mathematics and Philosophy of the Infinite},
 publisher	= {Harvard University Press},
 year		= 1979,
 isbn		= 0674348710}


@book{DavenportJH:comasa,
 author		= {Davenport, James and Siret, Y. and Tournier, E.},
 title		= {Computer Algebra: Systems and Algorithms
	for Algebraic Computation},
 publisher	= {Academic Press},
 year		= 1988,
 note		= {Translated from French; third edition 1993},
 isbn		= {0-12-204230-1}}


@book{DaveyBA:intlo,
 author		= {Davey, B. A. and Priestley, Hilary},
 title		= {Introduction to Lattices and Order},
 publisher	= {Cambridge University Press},
 year		= 1990}


@book{DavisM:undbpu,
 author		= {Davis, Martin},
 title		= {The Undecidable.
	Basic Papers on Undecidable, Unsolvable Problems and Computable Functions},
 publisher	= {Raven Press},
 address	= {Hewlett, N.Y.},
 year		= 1965}


@inproceedings{deBruijnNG:aut,
 author		= {de Bruijn, Nikolas},
 title		= {A Survey of the project {A}utomath},
 pages		= {579--606},
 crossref	= {CurryHB:hbcecl}}


@book{DedekindJWR:steiz,
 author		= {Dedekind, J. W. Richard},
 title		= {Stetigkeit und irrationale {Z}ahlen},
 publisher	= {Braunschweig},
 year		= 1872,
 note		= {Reprinted in \cite{DedekindJWR:gesmw}, pages 315--334;
	English translation, ``Continuity and Irrational Numbers''
	in \cite{DedekindJWR:esstn}}}


@book{DedekindJWR:wasssz,
 author		= {Dedekind, J. W. Richard},
 title		= {Was sind und was sollen die {Z}ahlen?},
 publisher	= {Braunschweig},
 year		= 1888,
 note		= {Reprinted in \cite{DedekindJWR:gesmw}, pages 335--391;
	English translation, ``The Nature and Meaning of Numbers''
	in \cite{DedekindJWR:esstn}}}


@book{DedekindJWR:esstn,
 author		= {Dedekind, J. W. Richard},
 title		= {Essays on the theory of numbers},
 publisher	= {Open Court},
 year		= 1901,
 note		= {English translations by Wooster Woodruff Beman;
	republished by Dover, 1963}}


@book{DedekindJWR:gesmw,
 author		= {Dedekind, J. W. Richard},
 title		= {Gesammelte mathematische {W}erke},
 publisher	= {Vieweg, Braunschweig},
 volume		= 3,
 year		= 1932,
 note		= {Edited by Robert Fricke, Emmy Noether and \O ystein Ore;
	republished by Chelsea, New York, 1969}}


@book{DetlefsenM:hilpem,
 author		= {Detlefsen, Michael},
 title		= {Hilbert's Program: an Essay on Mathematical
	Instrumentalism},
 publisher	= {Reidel},
 series		= {Synthese Library},
 number		= 182,
 year		= 1986,
 isbn		= 9027721513}


@book{DieudonneJA:panmpc,
 author		= {Dieudonn{\'e}, Jean Alexandre},
 title		= {Panorama des Math{\'e}matiques Pures:
	la Choix {B}ourbachique},
 publisher	= {Gauthier-Villars},
 year		= 1977,
 note		= {English translation,
	``A panorama of pure mathematics, as seen by N. Bourbaki''
	by I. G. Macdonald, Academic Press,
	Pure and Applied Mathematics, 97, 1982},
 isbn		= 0122155602}


@book{DieudonneJA:hisadt,
 author		= {Dieudonn{\'e}, Jean Alexandre},
 title		= {A History of Algebraic and Differential
	Topology 1900--1960},
 publisher	= {Birkh{\"a}user},
 year		= 1988,
 isbn		= {376433388X}}


@book{Dold:homa,
 author		= {Dold, Albrecht},
 title		= {Lectures on Algebraic Topology},
 publisher	= {Springer-Verlag},
 series		= {Grundlehren der mathematischen Wissenschaften},
 number		= 200,
 year		= 1972,
 isbn		= 3540057773}


@book{DummettMAE:elei,
 author		= {Dummett, Michael},
 title		= {Elements of Intuitionism},
 publisher	= {Oxford University Press},
 series		= {Logic Guides},
 year		= 1977,
 isbn		= 0198531583}


@book{DummettM:truoe,
 author		= {Dummett, Michael},
 title		= {Truth and Other Enigmas},
 publisher	= {Duckworth},
 address	= {London},
 year		= 1978}


@article{DyckhoffR:expmpp,
 author		= {Dyckhoff, Roy and Tholen, Walter},
 title		= {Exponentiable Maps, Partial Products and
	Pullback Complements},
 journal	= {Journal of Pure and Applied Algebra},
 volume		= 49,
 year		= 1987,
 pages		= {103--116}}


@proceedings{EckmannB:semtch,
 title		= {Seminar on Triples and Categorical Homology Theory},
 editor		= {Eckmann, Beno},
 booktitle	= {Seminar on Triples and Categorical Homology Theory},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 80,
 year		= 1969}


@book{EhresmanC:oevcc,
 author		= {Ehresman, Charles},
 title		= {\OE uvres compl\`etes et comment\'ees},
 publisher	= {Amiens},
 year		= {1980--84},
 note		= {Edited by Andr\'ee Charles Ehresmann;
	published as supplements to volumes 21--24 of
	\textit{Cahiers de topologie et g\'eom\'etrie
	diff\'erentielle}}}


@inproceedings{EhrhardtT:catsc,
 author		= {Ehrhardt, Thomas},
 title		= {Categorical Semantics of Constructions},
 editor		= {Gurevich, Yuri},
 booktitle	= {Logic in Computer Science~{III}},
 publisher	= {IEEE Computer Society Press},
 year		= 1988,
 pages		= {264--273}}


@inproceedings{EhrhardtT:dic,
 author		= {Ehrhardt, Thomas},
 title		= {Dictoses},
 pages		= {213--223},
 crossref	= {PittD:cattcs3}}


@book{EilenbergS:fouat,
 author		= {Eilenberg, Sammy and Steenrod, Norman},
 title		= {Foundations of Algebraic Topology},
 publisher	= {Princeton University Press},
 year		= 1952}


@proceedings{EilenbergS:catcfm,
 title		= {Categorical Algebra (La Jolla, 1965)},
 editor		= {Eilenberg, Sammy and Harrison, D. K. and Mac Lane, Saunders and R{\"o}hrl, Helmut},
 booktitle	= {Categorical Algebra (La Jolla, 1965)},
 publisher	= {Springer-Verlag},
 year		= 1966,
 callno		= {512.86 C74p},
 qmwlib		= {QA169 CON}}


@inproceedings{EilenbergS:cloc,
 author		= {Eilenberg, Sammy and Kelly, Max},
 title		= {Closed Categories},
 crossref	= {EilenbergS:catcfm}}


@book{EilenbergS:rec,
 author		= {Eilenberg, Sammy and Elgot, Calvin},
 title		= {Recursiveness},
 publisher	= {Academic Press},
 year		= 1970}


@book{EilenbergS:eilmlc,
 author		= {Eilenberg, Sammy and Mac Lane, Saunders},
 title		= {Eilenberg--{M}ac {L}ane, Collected Works},
 publisher	= {Academic Press},
 year		= 1986,
 isbn		= 0122340205}


@book{FauvelJG:hismr,
 author		= {Fauvel, John and Gray, Jeremy},
 title		= {The History of Mathematics, a Reader},
 publisher	= {Macmillan and the Open University},
 year		= 1987,
 isbn		= {0-333-42790-4, 0-333-42791-2}}


@proceedings{FenstadJE:scalc2,
 title		= {Second Scandinavian Logic Symposium},
 editor		= {Fenstad, Jens Erik},
 booktitle	= {Second Scandinavian Logic Symposium},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 number		= 63,
 year		= 1971}


@book{FerysR:dic,
 author		= {Feys, Richard and Fitch, Frederic},
 title		= {Dictionary of Symbols of Mathematical Logic},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 year		= 1969}


@article{FioreMP:domdsh,
 author		= {Fiore, Marcelo and Jung, Achim and Moggi, Eugenio and O'Hearn, Peter and Riecke, Jon and Rosolini, Giuseppe and Stark, Ian},
 title		= {Domains and Denotational Semantics: History,
	Accomplishments and Open Problems},
 journal	= {Bulletin of the EATCS},
 volume		= 59,
 year		= 1996,
 pages		= {227--256},
 url		= {http://www.brics.dk/~stark/papers/domdsh.html}}


@book{FitchFB:symli,
 author		= {Fitch, Frederic Benton},
 title		= {Symbolic Logic: an Introduction},
 publisher	= {Ronald Press},
 address	= {New York},
 year		= 1952}


@book{FittingMC:intlmt,
 author		= {Fitting, Melvin},
 title		= {Intuitionistic Logic, Model Theory and Forcing},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 year		= 1969}


@inproceedings{FloydR:assmp,
 author		= {Floyd, Robert},
 title		= {Assigning Meaning to Programs},
 editor		= {Schwartz, J. T.},
 booktitle	= {Mathematical Aspects of Computer Science},
 publisher	= {American Mathematical Society},
 series		= {Proceedings of Symposia in Applied Mathematics},
 number		= 19,
 year		= 1967,
 pages		= {19--32}}


@proceedings{FourmanMP:apps,
 title		= {Applications of Sheaves},
 editor		= {Fourman, Michael and Mulvey, Chris and Scott, Dana},
 booktitle	= {Applications of Sheaves},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 753,
 year		= 1979}


@proceedings{FourmanMP:appccs,
 title		= {Applications of categories in computer science},
 editor		= {Fourman, Michael and Johnstone, Peter and Pitts, Andrew},
 booktitle	= {Applications of categories in computer science},
 publisher	= {Cambridge University Press},
 series		= {London Mathematical Society Lecture Notes},
 number		= 177,
 year		= 1992}


@book{FowlerD:matpa,
 author		= {Fowler, David},
 title		= {The Mathematics of {P}lato's {A}cademy: a New Reconstruction},
 publisher	= {Oxford University Press},
 year		= 1987,
 isbn		= 0198539126}


@book{FraenkelA:foust,
 author		= {Fraenkel, Abraham and Bar-Hillel, Yehoshua},
 title		= {Foundations of Set Theory},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 year		= 1958}


@book{FregeG:trapwg,
 author		= {Frege, Gottlob},
 title		= {Translations from the Philosophical Writings of {G}ottlob {F}rege},
 publisher	= {Blackwell},
 year		= 1960,
 note		= {Edited by Peter Geach and Max Black; third edition, 1980}}


@book{FregeG:colpml,
 author		= {Frege, Gottlob},
 title		= {Collected Papers on Mathematics, Logic and Philosophy},
 publisher	= {Blackwell},
 year		= 1984,
 note		= {Edited by Brian McGinness}}


@book{FreydPJ:abec,
 author		= {Freyd, Peter},
 title		= {Abelian Categories: an Introduction to the
	Theory of Functors},
 publisher	= {Harper and Row},
 year		= 1964}


@inproceedings{FreydPJ:thefm,
 author		= {Freyd, Peter},
 title		= {The Theory of Functors and Models},
 editor		= {Addison, John and Henkin, Leon and Tarski, Alfred},
 booktitle	= {Theory of Models},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 year		= 1966,
 pages		= {107--120}}


@article{FreydPJ:aspt,
 author		= {Freyd, Peter},
 title		= {Aspects of Topoi},
 journal	= {Bulletin of the Australian Mathematical Society},
 volume		= 7,
 year		= 1972,
 pages		= {1--76 and 467--480}}


@article{FreydPJ:catcf1,
 author		= {Freyd, Peter and Kelly, Max},
 title		= {Categories of Continuous Functors,~{I}},
 journal	= {Journal of Pure and Applied Algebra},
 volume		= 2,
 year		= 1972,
 pages		= {169--191}}


@book{FreydPJ:cata,
 author		= {Freyd, Peter and Scedrov, Andre},
 title		= {Categories, Allegories},
 publisher	= {North-Holland},
 series		= {Mathematical Library},
 number		= 39,
 year		= 1990,
 isbn		= 0444703683}


@inproceedings{FreydPJ:algcc,
 author		= {Freyd, Peter},
 title		= {Algebraically Complete Categories},
 pages		= {95--104},
 crossref	= {CarboniA:comctc}}


@book{GabrielP:lokpk,
 author		= {Gabriel, Peter and Ulmer, Fritz},
 title		= {Lokal pr{\"a}sentierbare {K}ategorien},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 221,
 year		= 1971}


@book{GalileiG:2ns,
 author		= {Galilei, Galileo},
 title		= {Two New Sciences},
 year		= 1638,
 note		= {Translated by Stillman Drake,
	University of Wisconsin Press, 1974;
	Re-published by Wall \& Thompson, 1989},
 isbn		= 0921332203}


@book{GallierJH:logcs,
 author		= {Gallier, Jean},
 title		= {Logic for Computer Science: Foundations of Automated
	Theorem Proving},
 publisher	= {Harper and Row},
 series		= {Computer Science and Technology Series},
 year		= 1986,
 note		= {Republished by Wiley, 1987}}


@article{GandyRO:axie,
 author		= {Gandy, Robin},
 title		= {On the axiom of extensionality},
 journal	= {Journal of Symbolic Logic},
 volume		= 21,
 year		= 1956,
 pages		= {36--48 and 24:287--300}}


@article{GentzenG:untls,
 author		= {Gentzen, Gerhard},
 title		= {Untersuchungen {\"u}ber das {L}ogische {S}chliessen},
 journal	= {Mathematische Zeitschrift},
 volume		= 39,
 year		= 1935,
 pages		= {176--210 and 405--431},
 note		= {English translation in \cite{GentzenG:colpgg},
	pages 68--131.}}


@book{GentzenG:colpgg,
 author		= {Gentzen, Gerhard},
 title		= {The Collected Papers of {G}erhard {G}entzen},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 year		= 1969,
 note		= {Edited by M. E. Szabo}}


@book{GierzGK:comcl,
 author		= {Gierz, Gerhard and Hoffmann, Karl Heinrich and Keimel, Klaus and Lawson, Jimmie and Mislove, Michael and Scott, Dana},
 title		= {A Compendium of Continuous Lattices},
 publisher	= {Springer-Verlag},
 year		= 1980,
 isbn		= {354010111X}}


@book{GilliesDA:fredpf,
 author		= {Gillies, Donald},
 title		= {Frege, {D}edekind and {P}eano on the Foundations of Arithmetic},
 publisher	= {Van Gorcum},
 series		= {Methodology and Science Foundation},
 number		= 2,
 year		= 1982}


@incollection{GirardJY:uneelg,
 author		= {Girard, Jean-Yves},
 title		= {Une extension de l'interpretation de {G\"odel} {\`a} l'analyse,
	et son application {\`a} l'{\'e}limination des coupures
	dans l'analyse et la th{\'e}orie des types},
 pages		= {63--92},
 crossref	= {FenstadJE:scalc2}}


@article{GirardJY:linl,
 author		= {Girard, Jean-Yves},
 title		= {Linear Logic},
 journal	= {Theoretical Computer Science},
 volume		= 50,
 year		= 1987,
 pages		= {1--102}}


@book{GirardJY:protlc,
 author		= {Girard, Jean-Yves},
 title		= {Proof Theory and Logical Complexity},
 publisher	= {Bibliopolis},
 volume		= 1,
 year		= 1987,
 isbn		= 8870881237}


@book{GirardJY:prot,
 author		= {Girard, Jean-Yves and Lafont, Yves and Taylor, Paul},
 title		= {Proofs and Types},
 publisher	= {Cambridge University Press},
 series		= {Cambridge Tracts in Theoretical Computer Science},
 number		= 7,
 year		= 1989}


@book{GiraudJ:cohna,
 author		= {Giraud, Jean},
 title		= {Cohomologie non-ab\'elienne},
 publisher	= {Springer-Verlag},
 series		= {Grundlehren der mathematischen {W}issenschaften},
 number		= 179,
 year		= 1971,
 isbn		= 3540053077}


@inproceedings{GiraudJ:clat,
 author		= {Giraud, Jean},
 title		= {Classifying Topos},
 pages		= {43--56},
 crossref	= {LawvereFW:topagl}}


@article{GodelK:ubefus,
 author		= {G{\"o}del, Kurt},
 title		= {{\"U}ber formal unentscheidbare {S}{\"a}tze der
	{P}rincipia {M}athematica und verwandter {S}ysteme {I}},
 journal	= {Monatshefte f{\"u}r Mathematik und Physik},
 volume		= 38,
 year		= 1931,
 pages		= {173--198},
 note		= {English translations,
	``On Formally Undecidable Propositions of
	`{P}rincipia {M}athematica' and Related Systems''
	published by Oliver and Boyd, 1962 and Dover, 1992;
	also in \cite{vanHeijenoortJ:frofgs}, pages 596--616;
	also in \cite{DavisM:undbpu}, pages 5--38}}


@book{GodelK:colw,
 author		= {G{\"o}del, Kurt},
 title		= {Kurt G{\"o}del: Collected Works},
 booktitle	= {Kurt G{\"o}del: Collected Works},
 publisher	= {Oxford University Press},
 year		= 1980,
 note		= {Edited by Solomon Feferman and others},
 isbn		= 0195039645}


@book{Godement:topatf,
 author		= {Godement, Roger},
 title		= {Topologie Algebrique et Theorie des Faisceaux},
 publisher	= {Hermann},
 year		= 1958,
 isbn		= 2705612521}


@book{GoldblattR::topcal,
 author		= {Goldblatt, Robert},
 title		= {Topoi: The Categorial Analysis of Logic},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 number		= 98,
 year		= 1979,
 note		= {Third edition, 1983},
 isbn		= 0444852077}


@book{GrattanGuinnessI:frocst,
 title		= {From the Calculus to Set Theory, 1630--1910: an Introductory History},
 editor		= {Grattan-Guinness, Ivor},
 publisher	= {Duckworth},
 address	= {London},
 year		= 1980}


@book{GrattanGuinnessI:fonhms,
 title		= {The {F}ontana History of the Mathematical Sciences:
	the Rainbow of Mathematics},
 author		= {Grattan-Guinness, Ivor},
 publisher	= {Fontana},
 address	= {London},
 year		= 1997}


@book{GratzerG:unia,
 author		= {Gr{\"a}tzer, George},
 title		= {Universal Algebra},
 publisher	= {Van Nostrand},
 year		= 1968}


@inproceedings{GrayJW:fibcc,
 author		= {Gray, John},
 title		= {Fibred and Cofibred Categories},
 pages		= {21--83},
 crossref	= {EilenbergS:catcfm}}


@inproceedings{GrayW:frahst,
 author		= {Gray, John},
 title		= {Fragments of the History of Sheaf Theory},
 pages		= {1--79},
 crossref	= {FourmanMP:apps}}


@proceedings{GrayJW:catcsl,
 title		= {Categories in Computer Science and Logic},
 editor		= {Gray, John and Scedrov, Andre},
 booktitle	= {Categories in Computer Science and Logic},
 publisher	= {American Mathematical Society},
 series		= {Contemporary Mathematics},
 number		= 92,
 year		= 1989,
 isbn		= 0821851004}


@proceedings{GrothendieckA:semga1,
 title		= {S{\'e}minaire de G{\'e}ometrie Alg{\'e}brique,
	{I} (1960/1)},
 editor		= {Grothendieck, Alexander},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 224,
 year		= 1964}


@book{GunterCA:sempls,
 author		= {Gunter, Carl},
 title		= {Semantics of Programming Languages:
	Structures and Techniques},
 publisher	= {MIT Press},
 series		= {Foundations of Computing},
 year		= 1992,
 isbn		= 0262071436,
 lib_congr	= {QA76.7.G86 1992 005.13--dc20 92-10172}}


@book{HalmosPR:naist,
 author		= {Halmos, P{\'a}l},
 title		= {\Naive Set Theory},
 publisher	= {Van Nostrand},
 year		= 1960,
 note		= {Reprinted by Springer-Verlag,
	Undergraduate Texts in Mathematics, 1974},
 isbn		= 0387900926}


@book{HardyGH:mata,
 author		= {Hardy, G. H.},
 title		= {A Mathematician's Apology},
 publisher	= {Cambridge University Press},
 year		= 1940,
 note		= {Reprinted 1992}}


@book{HatcherWS:logfm,
 author		= {Hatcher, William},
 title		= {The Logical Foundations of Mathematics},
 publisher	= {Pergamon Press},
 series		= {Foundations and Philosophy of Science and Technology},
 year		= 1982,
 isbn		= {0-08-025800-x}}


@book{HausdorffF:grum,
 author		= {Hausdorff, Felix},
 title		= {{M}engenlehre},
 year		= 1914,
 note		= {English translation, ``Set Theory\tuck,''
	published by Chelsea, 1962}}


@book{HeckA:intm,
 author		= {Heck, Andr{\'e}},
 title		= {Introduction to {Maple}},
 publisher	= {Springer-Verlag},
 year		= 1993,
 note		= {Second edition, 1996},
 isbn		= {0-387-97662-0, 3-540-97662-0},
 lccn		= {QA155.7.E4H43 1993},
 mrclass	= {68Q40 (68T20)},
 mrnumber	= {94e:68087}}


@book{HeinzmannG:poirzp,
 title		= {Poincar{\'e}, {R}ussell, {Z}ermelo et {P}eano:
	Textes de la Discussion (1906--1912) sur
	les Fondements des Math{\'e}matiques:
	des Antinomies {\`a} la Pr\'edicativit{\'e}},
 editor		= {Heinzmann, Gerhard},
 booktitle	= {Poincar{\'e}, {R}ussell, {Z}ermelo at {P}eano:
	Textes de la Discussion (1906--1912) sur les Fondements des Math{\'e}matiques:
	des Antinomies {\`a} la Pr\'edicativit{\'e}},
 publisher	= {Albert Blanchard},
 address	= {Paris},
 year		= 1986}


@article{HennesseyM:alglnd,
 author		= {Hennessey, Matthew and Milner, Robin},
 title		= {Algebraic Laws for Non-determinism and Concurrency},
 journal	= {Journal of the ACM},
 volume		= 32,
 year		= 1975,
 pages		= {137--161}}


@book{HennessyM:algtp,
 author		= {Hennessy, Matthew},
 title		= {Algebraic Theory of Processes},
 publisher	= {MIT Press},
 series		= {Foundations of Computing},
 year		= 1988,
 isbn		= 0262081717}


@book{HennessyM:semple,
 author		= {Hennessy, Matthew},
 title		= {The Semantics of Programming Languages: an Elementary
	Introduction using Structural Operational Semantics},
 publisher	= {Wiley},
 year		= 1990,
 isbn		= 0471927724}


@book{HeytingA:int,
 author		= {Heyting, Arend},
 title		= {Intuitionism, an Introduction},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 year		= 1956,
 note		= {Revised edition, 1966}}


@book{HilbertD:grutlb,
 author		= {Hilbert, David and Ackermann, Wilhelm},
 title		= {Grundz{\"u}ge der theoretischen {L}ogik},
 publisher	= {Springer-Verlag},
 year		= 1928,
 note		= {Republished 1972;
	English translation by Lewis Hammond et al.,
	``Principles of Mathematical Logic\tuck,'' Chelsea, New York,
	1950}}


@book{HilbertD:grum,
 author		= {Hilbert, David and Bernays, Paul},
 title		= {Grundlagen der {M}athematik},
 publisher	= {Springer-Verlag},
 series		= {Grunlagen der Mathematischen Wissenschaften},
 number		= 40,
 year		= 1934}


@book{HilbertD:gesa,
 author		= {Hilbert, David},
 title		= {Gesammelte {A}bhandlungen},
 publisher	= {Springer-Verlag},
 volume		= 3,
 year		= 1935,
 note		= {Reprinted, 1970}}


@book{HiltonPJ:couha,
 author		= {Hilton, Peter and Stammbach, Urs},
 title		= {A Course in Homological Algebra},
 publisher	= {Springer-Verlag},
 series		= {Graduate Texts in Mathematics},
 number		= 4,
 year		= 1971,
 note		= {Second edition, 1997},
 isbn		= 0387948236}


@book{HindleyJR:intclc,
 author		= {Hindley, Roger and Seldin, Jonathan},
 title		= {Introduction or Combinators and Lambda Calculus},
 publisher	= {Cambridge University Press},
 series		= {London Mathematical Society Student Texts},
 number		= 1,
 year		= 1986,
 isbn		= {0-521-31839-4}}


@article{HoareCAR:axibcp,
 author		= {Hoare, Tony},
 title		= {An Axiomatic Basis for Computer Programming},
 journal	= {Communications of the ACM},
 volume		= 12,
 year		= 1969,
 pages		= {576--580 and 583}}


@book{HodgesW:modt,
 author		= {Hodges, Wilfrid},
 title		= {Model Theory},
 publisher	= {Cambridge University Press},
 series		= {Encyclopedia of Mathematics and its Applications},
 number		= 42,
 year		= 1993,
 isbn		= 0521304423}


@inproceedings{HofmannM:intttl,
 author		= {Hofmann, Martin},
 title		= {On the Interpretation of Type Theory in
	Locally Cartesian Closed Categories},
 editor		= {Pacholski, Leszek and Tiuryn, Jerzy},
 booktitle	= {Computer Science Logic {VIII}},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Computer Science},
 number		= 933,
 year		= 1995,
 pages		= {427--441},
 isbn		= 0387600175}


@book{HofstadterDR:godeb,
 author		= {Hofstadter, Dougals},
 title		= {G{\"o}del, {E}scher, {B}ach, and Eternal Golden Braid},
 publisher	= {Harvester},
 year		= 1979,
 note		= {Reprinted by Penguin, 1980},
 isbn		= {0-14-017997-6}}


@incollection{HowardWA:fortnc,
 author		= {Howard, William},
 title		= {The formulae-as-types notion of construction},
 pages		= {479--490},
 crossref	= {CurryHB:hbcecl}}


@article{HuetGP:undutol,
 author		= {Huet, G{\'e}rard},
 title		= {The Undecidability of Unification in Third Order Logic},
 journal	= {Information and Control},
 volume		= 22,
 number		= 3,
 month		= apr,
 year		= 1973,
 pages		= {257--267}}


@article{HuetGP:uniatl,
 author		= {Huet, G{\'e}rard},
 title		= {A Unification Algorithm for Typed Lambda Calculus},
 journal	= {Theoretical Computer Science},
 volume		= 1,
 year		= 1975,
 pages		= {27--57}}


@article{HylandJME:trit,
 author		= {Hyland, Martin and Johnstone, Peter and Pitts, Andrew},
 title		= {Tripos Theory},
 journal	= {Mathematical Proceedings of the Cambridge Philosophical Society},
 volume		= 88,
 year		= 1980,
 pages		= {205--232}}


@inproceedings{HylandJME:funscl,
 author		= {Hyland, Martin},
 title		= {Function Spaces in the Category of Locales},
 editor		= {Banachewski, Bernhard and Hoffman, Rudolf-Eberhard},
 booktitle	= {Continuous Lattices},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 871,
 year		= 1981,
 pages		= {264--281},
 isbn		= {3-540-10848-3}}


@incollection{HylandJME:efft,
 author		= {Hyland, Martin},
 title		= {The Effective Topos},
 pages		= {165--216},
 crossref	= {TroelstraAS:lejbcs}}


@article{HylandJME:smacc,
 author		= {Hyland, Martin},
 title		= {A Small Complete Category},
 journal	= {Annals of Pure and Applied Logic},
 volume		= 40,
 year		= 1988,
 pages		= {135--165}}


@inproceedings{PittsAM:theccs,
 author		= {Hyland, Martin and Pitts, Andrew},
 title		= {The Theory of Constructions: Categorical Semantics and
	Topos-Theoretic Models},
 pages		= {137--199},
 crossref	= {GrayJW:catcsl}}


@article{HylandJME:disoet,
 author		= {Hyland, Martin and Robinson, Edmund and Rosolini, Giuseppe},
 title		= {The Discrete Objects in the Effective Topos},
 journal	= {Proceedings of the London Mathematical Society},
 volume		= 60,
 year		= 1990,
 pages		= {1--36}}


@phdthesis{JacobsB:phd,
 author		= {Jacobs, Bart},
 title		= {Categorical Type Theory},
 school		= {Universiteit Nijmegen},
 year		= 1990}


@inproceedings{JacobsB:relmit,
 author		= {Jacobs, Bart and Moggi, Eugenio and Streicher, Thomas},
 title		= {Relating Models of Impredicative Type Theories},
 year		= 1991,
 pages		= {197--218},
 crossref	= {PittD:cattcs4}}


@article{JacobsB:comcst,
 author		= {Jacobs, Bart},
 title		= {Comprehension categories and the semantics of type dependency},
 journal	= {Theoretical Computer Science},
 volume		= 107,
 number		= 2,
 year		= 1993,
 pages		= {169--207}}


@article{JaskowskiS:rulsfl,
 author		= {J{\'a}skowski, Stanis{\l}aw},
 title		= {On the Rules of Suppositions in Formal Logic},
 journal	= {Studia Logica},
 volume		= 1,
 year		= 1934,
 note		= {Reprinted in \cite{McCallS:poll}, pages 232--258}}


@book{JeckT:sett,
 author		= {Jech, Thomas},
 title		= {Set Theory},
 publisher	= {Academic Press},
 series		= {Pure and Applied Mathematics},
 number		= 79,
 year		= 1978,
 note		= {Second edition, 1997},
 isbn		= 0123819504}


@book{JohnstonePT:topt,
 author		= {Johnstone, Peter},
 title		= {Topos Theory},
 publisher	= {Academic Press},
 series		= {London Mathematical Society Monographs},
 number		= 10,
 year		= 1977,
 isbn		= 0123878500}


@book{JohnstonePT:indca,
 author		= {Johnstone, Peter and Par{\'e}, Robert and Roseburgh, Robert and Schumacher, Steve and Wood, Richard and Wraith, Gavin},
 title		= {Indexed Categories and their Applications},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 661,
 year		= 1978}


@book{JohnstonePT:stos,
 author		= {Johnstone, Peter},
 title		= {Stone Spaces},
 publisher	= {Cambridge University Press},
 series		= {Cambridge Studies in Advanced Mathematics},
 number		= 3,
 year		= 1982,
 isbn		= 0521238935}


@article{JohnstonePT:whevt,
 author		= {Johnstone, Peter},
 title		= {When is a Variety a Topos?},
 journal	= {Algebra Universalis},
 volume		= 21,
 year		= 1985,
 pages		= {198--212}}


@article{JohnstonePT:coltccv,
 author		= {Johnstone, Peter},
 title		= {Collapsed Toposes and Cartesian Closed Varieties},
 journal	= {Journal of Algebra},
 volume		= 129,
 year		= 1990,
 pages		= {446--480}}


@article{JoyalA:extgtg,
 author		= {Joyal, Andr{\'e} and Tierney, Myles},
 title		= {An Extension of the {G}alois Theory of {G}rothendieck},
 journal	= {Memoirs of the American Mathematical Society},
 volume		= 51,
 number		= 309,
 year		= 1984}


@inproceedings{JoyalA:fonaes,
 author		= {Joyal, Andr{\'e}},
 title		= {Foncteurs Analytiques et Esp\`eces de Structures},
 editor		= {Labelle, Gilbert and Leroux, Pierre},
 booktitle	= {Combinatoire \'enumerative},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 1234,
 year		= 1987,
 pages		= {126--159}}


@book{JoyalA:algst,
 author		= {Joyal, Andr{\'e} and Moerdijk, Ieke},
 title		= {Algebraic Set Theory},
 publisher	= {Cambridge University Press},
 series		= {London Mathematical Society Lecture Notes},
 number		= 220,
 year		= 1995,
 isbn		= 0521558301}


@article{JungA:carccac,
 author		= {Jung, Achim},
 title		= {Cartesian Closed Categories of Algebraic {CPO's}},
 journal	= {Theoretical Computer Science},
 volume		= 70,
 year		= 1990,
 pages		= {233--250}}


@book{KampH:disli,
 author		= {Kamp, Hans and Reyle, Uwe},
 title		= {From Discourse to Logic:
	Introduction to Model-theoretic Semantics of Natural Language, Formal
	Logic and Discourse Representation Theory},
 publisher	= {Reidel},
 year		= 1991,
 note		= {Re-published by Kluwer,
	Studies in Linguistics and Philosophy, 42,
	1993},
 isbn		= {079232403X}}


@article{KanDM:adjf,
 author		= {Kan, Daniel},
 title		= {Adjoint Functors},
 journal	= {Transactions of the American Mathematical Society},
 volume		= 87,
 year		= 1958,
 pages		= {294--329}}


@book{KelleyJL:gent,
 author		= {Kelley, John},
 title		= {General Topology},
 publisher	= {Van Nostrand},
 year		= 1955,
 note		= {Reprinted by Springer-Verlag,
	Graduate Texts in Mathematics, 27, 1975},
 isbn		= 0387901256}


@article{KellyGM:monep,
 author		= {Kelly, Max},
 title		= {Monomorphisms, Epimorphisms and Pull-backs},
 journal	= {Journal of the Australian Mathematical Society},
 volume		= 9,
 year		= 1969,
 pages		= {124--142}}


@book{KellyGM:catsps,
 title		= {Proceedings of the Sydney Category Theory Seminar 1972--3},
 editor		= {Kelly, Max},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 420,
 year		= 1974,
 isbn		= 3540069666}


@book{KellyGM:bascec,
 author		= {Kelly, Max},
 title		= {Basic Concepts of Enriched Category Theory},
 publisher	= {Cambridge University Press},
 series		= {London Mathematical Society Lecture Notes},
 number		= 64,
 year		= 1982,
 isbn		= 0521287022}


@book{KleeneSC:intm,
 author		= {Kleene, Stephen},
 title		= {Introduction to Metamathematics},
 publisher	= {North-Holland},
 series		= {Bibliotheca mathematica},
 number		= 1,
 year		= 1952,
 note		= {Revised edition, Wolters-Noordhoff, 1971}}


@book{KleeneS:fouime,
 author		= {Kleene, Stephen and Vesley, Richard},
 title		= {The Foundations of Intuitionistic Mathematics,
	Especially in relation to Recursive Functions},
 publisher	= {North-Holland},
 year		= 1965}


@book{KleeneSC:matl,
 author		= {Kleene, Stephen},
 title		= {Mathematical Logic},
 publisher	= {John Wiley and Sons},
 year		= 1967}


@book{KnuthDE:artcp,
 author		= {Knuth, Donald},
 title		= {The Art of Computer Programming},
 publisher	= {Addison-Wesley},
 year		= 1968,
 note		= {Three volumes published out of seven planned;
	second edition, 1973}}


@inproceedings{KnuthDE:simwpu,
 author		= {Knuth, Donald and Bendix, Peter},
 title		= {Simple Word Problems in Universal Algebra},
 editor		= {Leech, John},
 booktitle	= {Computational Problems in Abstract Algebra},
 publisher	= {Pergamon Press},
 year		= 1970,
 pages		= {263--297}}


@book{KnuthDE:surn,
 author		= {Knuth, Donald},
 title		= {Surreal Numbers},
 publisher	= {Addison-Wesley},
 year		= 1974}


@book{KockA:syndg,
 author		= {Kock, Anders},
 title		= {Synthetic Differential Geometry},
 publisher	= {Cambridge University Press},
 series		= {London Mathematical Society Lecture Notes},
 number		= 51,
 year		= 1981,
 isbn		= 0521241383}


@article{KockA:monsau,
 author		= {Kock, Anders},
 title		= {Monads for which Structures are Adjoint to Units},
 journal	= {Journal of Pure and Applied Algebra},
 volume		= 104,
 year		= 1995,
 pages		= {41--59}}


@article{KolmogorovAN:priem,
 author		= {Kolmogorov, Andrei},
 title		= {On the Principle of Excluded Middle},
 journal	= {Matemati\v ceskii Sbornik},
 volume		= 32,
 year		= 1925,
 pages		= {646--667},
 note		= {In Russian;
	English translation in \cite{vanHeijenoortJ:frofgs}, pages 414--437}}


@article{KoymansCPJ:modlc,
 author		= {Koymans, C. P. J.},
 title		= {Models of the Lambda Calculus},
 journal	= {Information and Control},
 volume		= 52,
 year		= 1982,
 pages		= {206--332}}


@article{KreiselG:matscp,
 author		= {Kreisel, Georg},
 title		= {Mathematical significance of consistency proofs},
 journal	= {Journal of Symbolic Logic},
 volume		= 23,
 year		= 1958,
 pages		= {155--182}}


@inproceedings{KreiselG:infrcp,
 author		= {Kreisel, Georg},
 title		= {Informal Rigour and Completeness Proofs},
 editor		= {Lakatos, Imre},
 booktitle	= {Problems in the Philosophy of Mathematics},
 publisher	= {North-Holland},
 year		= 1967}


@article{KreiselG:surpt,
 author		= {Kreisel, Georg},
 title		= {A Survey of Proof Theory},
 journal	= {Journal of Symbolic Logic},
 volume		= 33,
 year		= 1968,
 pages		= {321--388}}


@incollection{KreiselG:surpt2,
 author		= {Kreisel, Georg},
 title		= {A Survey of Proof Theory {II}},
 pages		= {109--170},
 crossref	= {FenstadJE:scalc2}}


@book{KretzmannN:camhlm,
 title		= {The Cambridge history of later medieval philosophy:
	from the rediscovery of Aristotle
	to the disintegration of scholasticism, 1100-1600},
 editor		= {Kretzmann, Norman and Kenny, Anthony and Pinborg, Jan},
 publisher	= {Cambridge University Press},
 year		= 1982,
 isbn		= 0521226058}


@book{KuratowskiK:sett,
 author		= {Kuratowski, Kazimierz and Mostowski, Andrzej},
 title		= {Teoria mnogosci},
 publisher	= {Polish Scientific Publishers},
 year		= 1966,
 note		= {English translation, ``Set Theory'' by M. Maczynski,
	North-Holland, Studies in Logic and the Foundations of Mathematics,
	number 86, 1968; second edition, 1976}}


@phdthesis{LafontYGA:logcm,
 author		= {Lafont, Yves},
 title		= {Logiques, Cat{\'e}gories et Machines},
 school		= {Universit{\'e} de Paris 7},
 year		= 1987}


@inproceedings{LafontYGA:gamsll,
 author		= {Lafont, Yves and Streicher, Thomas},
 title		= {Game Semantics for Linear Logic},
 booktitle	= {Logic in Computer Science VI},
 publisher	= {IEEE Computer Society Press},
 year		= 1991,
 pages		= {43--50}}


@article{LairC:dialle,
 author		= {Lair, Christian},
 title		= {Diagrammes Localement Libres, Extensions de Corps et Th\'eorie
	de {G}alois},
 journal	= {Diagrammes},
 volume		= 10,
 year		= 1983}


@article{LakatosI:pror,
 author		= {Lakatos, Imre},
 title		= {Proofs and Refutations: the Logic of Mathematical Discovery},
 journal	= {British Journal for the Philosophy of Science},
 volume		= 14,
 year		= 1963,
 pages		= {1--25},
 note		= {Edited by John Worrall and Elie Zahar,
	Cambridge University Press, 1976}}


@book{LakoffG:womfdt,
 author		= {Lakoff, George},
 title		= {Women, Fire, and Dangerous Things:
	What Categories Reveal about the Mind},
 publisher	= {University of Chicago Press},
 year		= 1986,
 isbn		= 0226468046}


@article{LambekJ:matss,
 author		= {Lambek, Joachim},
 title		= {The Mathematics of Sentence Structure},
 journal	= {American Mathematical Monthly},
 volume		= 65,
 year		= 1958,
 pages		= {154--170}}


@article{LambekJ:dedsc1,
 author		= {Lambek, Joachim},
 title		= {Deductive Systems and Categories {I}: Syntactic
	Calculus and Residuated Categories},
 journal	= {Mathematical Systems Theory},
 volume		= 2,
 year		= 1968,
 pages		= {287--318}}


@incollection{LambekJ:dedsc2,
 author		= {Lambek, Joachim},
 title		= {Deductive Systems and Categories {II}: Standard
	Constructions and Closed Categories},
 editor		= {Hilton, Peter},
 booktitle	= {Category Theory, Homology Theory and their Applications},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 86,
 year		= 1969,
 pages		= {76--122}}


@incollection{LambekJ:dedsc3,
 author		= {Lambek, Joachim},
 title		= {Deductive Systems and Categories {III}: Cartesian
	Closed Categories, Intuitionist Propositional Calculus,
	and Combinatory Logic},
 pages		= {57--82},
 crossref	= {LawvereFW:topagl}}


@article{LambekJ:intttf,
 author		= {Lambek, Joachim and Scott, Philip J.},
 title		= {Intuitionist Type Theory and the Free Topos},
 journal	= {Journal of Pure and Applied Algebra},
 volume		= 19,
 year		= 1980,
 pages		= {215--257}}


@book{LambekJ:inthoc,
 author		= {Lambek, Joachim and Scott, Philip},
 title		= {Introduction to Higher Order Categorical Logic},
 publisher	= {Cambridge University Press},
 series		= {Cambridge Studies in Advanced Mathematics},
 number		= 7,
 year		= 1986,
 isbn		= 0521246652}


@inproceedings{LambekJ:mulr,
 author		= {Lambek, Joachim},
 title		= {Multicategories Revisited},
 pages		= {217--240},
 crossref	= {GrayJW:catcsl}}


@book{LangS:intla,
 author		= {Lang, Serge},
 title		= {Introduction to linear algebra.},
 publisher	= {Addison-Wesley},
 year		= 1970,
 note		= {Third edition, Springer-Verlag, Undergraduate Texts
	in Mathematics, 1987},
 isbn		= 3540962050}


@article{LawvereFW:funsat,
 author		= {Lawvere, Bill},
 title		= {Functorial Semantics of Algebraic Theories},
 journal	= {Proceedings of the National Academy of Sciences
	of the United States of America},
 volume		= 50,
 number		= 1,
 year		= 1963,
 pages		= {869--872}}


@article{LawvereFW:eletcs,
 author		= {Lawvere, Bill},
 title		= {An Elementary Theory of the Category of Sets},
 journal	= {Proceedings of the National Academy of Sciences
	of the United States of America},
 volume		= 52,
 year		= 1964,
 pages		= {1506--1511}}


@inproceedings{LawvereFW:catcfm,
 author		= {Lawvere, William},
 title		= {The Category of Categories as a Foundation for Mathematics},
 pages		= {1--20},
 crossref	= {EilenbergS:catcfm}}


@inproceedings{LawvereFW:diaacc,
 author		= {Lawvere, Bill},
 title		= {Diagonal Arguments and Cartesian Closed Categories},
 editor		= {Hilton, Peter},
 booktitle	= {Category Theory, Homology Theory and their Applications II},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 92,
 year		= 1968,
 pages		= {134--145}}


@inproceedings{LawvereFW:somapc,
 author		= {Lawvere, Bill},
 title		= {Some Algebraic Problems in the Context of Functorial
	Semantics of Algebraic Structures},
 editor		= {{Mac Lane}, Saunders},
 booktitle	= {Reports of the Midwest Category Seminar~{II}},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 61,
 year		= 1968,
 pages		= {41--61}}


@article{LawvereFW:adjf,
 author		= {Lawvere, Bill},
 title		= {Adjointness in Foundations},
 journal	= {Dialectica},
 volume		= 23,
 year		= 1969,
 pages		= {281--296}}


@inproceedings{LawvereFW:equhcs,
 author		= {Lawvere, Bill},
 title		= {Equality in Hyperdoctrines and the Comprehension Schema
	as an Adjoint Functor},
 editor		= {Heller, Alex},
 booktitle	= {Applications of Categorical Algebra},
 publisher	= {American Mathematical Society},
 series		= {Proceedings of Symposia in Pure Mathematics},
 number		= 17,
 year		= 1970,
 pages		= {1--14}}


@inproceedings{LawvereFW:quas,
 author		= {Lawvere, Bill},
 title		= {Quantifiers and Sheaves},
 booktitle	= {Actes du {C}ongr\`es International des Math{\'e}maticiens},
 publisher	= {Gauthier-Villars},
 volume		= 1,
 year		= 1971,
 pages		= {329--334}}


@proceedings{LawvereFW:topagl,
 title		= {Toposes, Algebraic Geometry, and Logic},
 editor		= {Lawvere, Bill},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 274,
 year		= 1972}


@inproceedings{LawvereFW:metsgl,
 author		= {Lawvere, Bill},
 title		= {Metric Spaces, Generalised Logic, and Closed Categories},
 booktitle	= {Rendiconti del Seminario Matematico e Fisico di Milano},
 publisher	= {Tipografia Fusi, Pavia},
 volume		= 43,
 year		= 1973}


@proceedings{LawvereFW:modtt,
 title		= {Model Theory and Topoi},
 editor		= {Lawvere, Bill and Maurer, Christian and Wraith, Gavin},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 445,
 year		= 1975,
 isbn		= 0387071644}


@book{LawvereFW:conmfi,
 author		= {Lawvere, Bill and Schanuel, Stephen},
 title		= {Conceptual Mathematics: a First Introduction to Categories},
 publisher	= {Cambridge University Press},
 year		= 1997,
 isbn		= 0521472490}


@article{SmythMB:algsdt,
 author		= {Lehmann, Daniel and Smyth, Michael},
 title		= {Algebraic Specifications of Data Types: a Synthetic Approach},
 journal	= {Mathematical Systems Theory},
 volume		= 14,
 year		= 1981,
 pages		= {97--139}}


@incollection{LeivantD:conpp,
 author		= {Leivant, Daniel},
 title		= {Contracting Proofs to Programs},
 pages		= {279--327},
 crossref	= {OdifreddiP:logcs}}


@book{LewisCI:sursl,
 author		= {Lewis, Clarence},
 title		= {A Survey of Symbolic Logic},
 publisher	= {University of California Press},
 year		= 1918,
 note		= {Republished by Dover, 1960}}


@book{LiderholmC:matmd,
 author		= {Linderholm, Carl},
 title		= {Mathematics made Difficult},
 publisher	= {Wolfe},
 address	= {London},
 year		= 1971}


@incollection{LintonFEJ:outfs,
 author		= {Linton, Fred},
 title		= {An Outline of Functorial Semantics},
 pages		= {7--52},
 crossref	= {EckmannB:semtch}}


@book{LukasiewiczJ:arissm,
 author		= {{\L}ukasiewicz, Jan},
 title		= {Aristotle's Syllogistic
	from the Standpoint of Modern Formal Logic},
 publisher	= {Oxford University Press},
 year		= 1951,
 note		= {Second edition, 1963}}


@book{LukasiewiczJ:eleml,
 author		= {{\L}ukasiewicz, Jan},
 title		= {Elements of Mathematical Logic},
 publisher	= {Pergamon Press},
 year		= 1963,
 note		= {Translated from Polish by Olgierd Wojtasiewicz}}


@book{LukasiewiczJ:janlsw,
 author		= {{\L}ukasiewicz, Jan},
 title		= {Selected Works},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 year		= 1970,
 note		= {Edited by Ludwig Berkowski},
 isbn		= 0720422523}


@inproceedings{LuoZ:unitdt,
 author		= {Luo, Zhaohui},
 title		= {A Unifying Theory of Dependent Types:
	the Schematic Approach},
 editor		= {Nerode, Anil and Taitslin, Mikhail},
 booktitle	= {Logical Foundations of Computer Science
	(Logic at Tver '92)},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Computer Science},
 number		= 620,
 year		= 1992,
 pages		= {293--304}}


@book{MacCallumMAH:algcwr,
 author		= {MacCallum, Malcolm and Wright, Francis},
 title		= {Algebraic Computing with {REDUCE}: lecture notes from
	the First Brazilian School on Computer Algebra},
 publisher	= {Oxford University Press},
 year		= 1991,
 isbn		= 0198536461}


@book{BirkhoffG:alg,
 author		= {Mac Lane, Saunders and Birkhoff, Garrett},
 title		= {Algebra},
 publisher	= {MacMillan},
 address	= {New York},
 year		= 1967,
 note		= {Second edition, 1979}}


@book{MacLaneS:catwm,
 author		= {Mac Lane, Saunders},
 title		= {Categories for the Working Mathematician},
 publisher	= {Springer-Verlag},
 series		= {Graduate Texts in Mathematics},
 number		= 5,
 year		= 1971,
 isbn		= 0387900357}


@article{MacLaneS:matmsp,
 author		= {Mac Lane, Saunders},
 issn		= {0002-9890},
 journal	= {American Mathematical Monthly},
 mrclass	= {00A25},
 mrnumber	= {83d:00017},
 mrreviewer	= {F. J. Murray},
 pages		= {462--472},
 title		= {Mathematical Models: a Sketch for the Philosophy of
	Mathematics},
 volume		= 88,
 year		= 1981}


@book{MacLaneS:selp,
 author		= {Mac Lane, Saunders},
 title		= {Selected Papers},
 publisher	= {Springer-Verlag},
 year		= 1979,
 note		= {Edited by Irving Kaplansky},
 isbn		= 0387903941}


@book{MacLaneS:matff,
 author		= {Mac Lane, Saunders},
 title		= {Mathematics, Form and Function},
 publisher	= {Springer-Verlag},
 year		= 1986,
 isbn		= 0387962174}


@incollection{MacLaneS:catcp,
 author		= {Mac Lane, Saunders},
 title		= {Categories and Concepts in Perspective},
 editor		= {Duren, Peter and Askey, Richard and Merzbach, Uta},
 booktitle	= {A Century of Mathematics in America},
 publisher	= {American Mathematical Society},
 volume		= 1,
 year		= 1988,
 pages		= {323--365},
 note		= {Addendum in volume 3, pages 439--441},
 isbn		= 0821801244}


@book{MacLaneS:shegl,
 author		= {Mac Lane, Saunders and Moerdijk, Ieke},
 title		= {Sheaves in Geometry and Logic:
	a First Introduction to Topos Theory},
 publisher	= {Springer-Verlag},
 series		= {Universitext},
 year		= 1992,
 isbn		= 0387977104}


@book{MakkaiM:firocl,
 author		= {Makkai, Michael and Reyes, Gonzalo},
 title		= {First Order Categorical Logic: Model-Theoretical
	Methods in the Theory of Topoi and Related Categories},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 611,
 year		= 1977}


@article{MakkaiM:somrlf,
 author		= {Makkai, Michael and Pitts, Andrew},
 title		= {Some Results on Locally Finitely Presentable Categories},
 journal	= {Transactions of the American Mathematical Society},
 volume		= 299,
 year		= 1987,
 pages		= {473--496}}


@article{MakkaiM:stodfo,
 author		= {Makkai, Michael},
 title		= {Stone Duality for First Order Logic},
 journal	= {Advances in Mathematics},
 volume		= 65,
 year		= 1987,
 pages		= {97--170}}


@book{MakkaiM:acccfc,
 author		= {Makkai, Michael and Par{\'e}, Robert},
 title		= {Accessible Categories: the Foundations of Categorical
	Model Theory},
 publisher	= {American Mathematical Society},
 series		= {Contemporary Mathematics},
 number		= 104,
 year		= 1990,
 isbn		= {082185111X}}


@article{MakkaiM:fibfip,
 author		= {Makkai, Michael},
 title		= {The Fibrational Formulation of Intuitionistic
	Predicate Logic},
 journal	= {Notre Dame Journal of Formal Logic},
 volume		= 34,
 year		= 1993,
 pages		= {334--7 and 471--498}}


@article{MakkaiM:avoacc,
 author		= {Makkai, Michael},
 title		= {Avoiding the Axiom of Choice in Category Theory},
 journal	= {Journal of Pure and Applied Algebra},
 volume		= 108,
 year		= 1996,
 pages		= {109--173}}


@unpublished{MakkaiM:firold,
 author		= {Makkai, Michael},
 title		= {First Order Logic with Dependent Sorts},
 year		= 1997,
 note		= {\texttt{ftp.math.mcgill.ca}}}


@book{MalcevA:metasc,
 author		= {Mal'cev, Anatolii},
 title		= {The Metamathematics of Algebraic Systems.
	Collected Papers 1936--67},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 number		= 66,
 year		= 1971,
 note		= {Edited by Benjamin Wells}}


@book{MancosuP:frobh,
 author		= {Mancosu, Paolo},
 title		= {From {B}rouwer to {H}ilbert:
	the Debate on the Foundations of Mathematics in the 1920s},
 booktitle	= {From {B}rouwer to {H}ilbert:
	the Debate on the Foundations of Mathematics in the 1920s},
 publisher	= {Oxford University Press},
 year		= 1998,
 isbn		= {0-19-509632-0},
 lccn		= {QA8.6.F757 511'.2--dc20 96-32918}}


@book{ManesE:algt,
 author		= {Manes, Ernest},
 title		= {Algebraic Theories},
 publisher	= {Springer-Verlag},
 series		= {Graduate Texts in Mathematics},
 number		= 26,
 year		= 1976,
 isbn		= {038790140X}}


@article{MarmolejoF:confc,
 author		= {Marmolejo, Francisco},
 title		= {Continuous Families of Coalgebras},
 journal	= {Journal of Pure and Applied Algebra},
 volume		= 130,
 year		= 1998,
 pages		= {197--215}}


@inproceedings{MartinLofP:intttp,
 author		= {Martin-L{\"o}f, Per},
 title		= {An Intuitionistic Theory of Types: Predicative part},
 editor		= {Rose, Harvey and Sheperdson, John},
 booktitle	= {Logic Colloquium '73},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 number		= 80,
 year		= 1975,
 pages		= {73--118}}


@book{MartinLofP:inttt,
 author		= {Martin-L{\"o}f, Per},
 title		= {Intuitionistic Type Theory},
 publisher	= {Bibliopolis},
 address	= {Naples},
 year		= 1984}


@book{MathiasARD:camssm,
 title		= {Cambridge Summer School in Mathematical Logic},
 editor		= {Mathias, Adrian and Rogers, Hartley},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 337,
 year		= 1973}


@book{McCallS:poll,
 author		= {McCall, Storrs},
 title		= {Polish Logic, 1920-1939},
 publisher	= {Oxford University Press},
 year		= 1967}


@book{McKenzieRN:comtcm,
 author		= {McKenzie, Ralph and Freese, Ralph},
 title		= {Commutator Theory for Congruence Modular Varieties},
 publisher	= {Cambridge University Press},
 series		= {London Mathematical Society Lecture Notes},
 number		= 125,
 year		= 1987,
 isbn		= 0521348323}


@book{McKenzieRN:alglv,
 author		= {McKenzie, Ralph and McNulty, George and Taylor, Walter},
 title		= {Algebras, Lattices, Varieties},
 publisher	= {Wadsworth and Brooks},
 year		= 1987,
 isbn		= 0534076513}


@book{McLartyC:elecet,
 author		= {McLarty, Colin},
 title		= {Elementary Categories, Elementary Toposes},
 publisher	= {Oxford University Press},
 series		= {Logic Guides},
 number		= 21,
 year		= 1992,
 isbn		= 0198533926}


@article{MillerD:unipfl,
 author		= {Miller, Dale and Nadathur, Gopalan and Pfenning, Frank and Scedrov, Andre},
 title		= {Uniform Proofs as a Foundation for Logic Programming},
 journal	= {Annals of Pure and Applied Logic},
 volume		= 51,
 year		= 1991,
 pages		= {125--137}}


@book{MitchellB:thec,
 author		= {Mitchell, Barry},
 title		= {Theory of Categories},
 publisher	= {Academic Press},
 series		= {Pure and Applied Mathematics},
 number		= 17,
 year		= 1965}


@inproceedings{MitchellJC:notsr,
 author		= {Mitchell, John and Scedrov, Andre},
 title		= {Notes on Sconing and Relators},
 editor		= {B{\"o}rger, Egon and J{\"a}ger, Gerhard and B{\"u}ning, Hans and Richter, Michael},
 booktitle	= {Computer Science Logic '92},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Computer Science},
 number		= 702,
 year		= 1993,
 pages		= {352--378}}


@book{MitchellJC:foupl,
 author		= {Mitchell, John},
 title		= {Foundations for Programming Languages},
 publisher	= {MIT Press},
 year		= 1996,
 isbn		= 0262133210}


@article{MoggiE:notcm,
 author		= {Moggi, Eugenio},
 title		= {Notions of Computation and Monads},
 journal	= {Information and Computation},
 volume		= 93,
 year		= 1991,
 pages		= {55--92}}


@inproceedings{MontagueR:fraaaz,
 author		= {Montague, Richard},
 title		= {Fraenkel's Addition to the Axioms of {Z}ermelo},
 pages		= {91--114},
 note		= {},
 crossref	= {BarHillelY:essfm}}


@book{MooreGH:zerac,
 author		= {Moore, Gregory},
 title		= {Zermelo's Axiom of Choice:
	its Origins, Development, and Influence},
 publisher	= {Springer-Verlag},
 series		= {Studies in the History of Mathematics and Physical Science},
 number		= 8,
 year		= 1982,
 isbn		= 0387906703}


@article{Myhill:effopr,
 author		= {Myhill, John and Shepherson, John},
 title		= {Effective Operations on Partial Recursive Functions},
 journal	= {Zeitschrift f{\"u}r Mathematische Logik
	und Gr{\"u}ndlagen der Mathematik},
 year		= 1955,
 pages		= {310--317},
 volme		= 1}


@book{NeumannPM:grog,
 author		= {Neumann, Peter and Stoy, Gabrielle and Thompson, Edward},
 title		= {Groups and Geometry},
 publisher	= {Oxford University Press},
 year		= 1993}


@article{NiefieldS:jpaa,
 author		= {Niefield, Susan},
 title		= {Cartesianness: Topological Spaces, Uniform Spaces
	and Affine Varieties},
 journal	= {Journal of Pure and Applied Algebra},
 volume		= 23,
 year		= 1982,
 pages		= {147--167}}


@book{NoetherE:gesa,
 author		= {Noether, Emmy},
 title		= {Gesammelte {A}bhandlungen},
 publisher	= {Springer-Verlag},
 year		= 1983,
 note		= {Edited by Nathan Jabobson}}


@book{NordstromB:promtt,
 author		= {Nordstr{\"o}m, Bengt and Petersson, Kent and Smith, Jan},
 title		= {Programming in {M}artin-{L}\"{o}f's Type Theory:
	an Introduction},
 publisher	= {Oxford University Press},
 series		= {International Series of Monographs on Computer Science},
 number		= 7,
 year		= 1990}


@article{ObtulowiczA:cataam,
 author		= {Obtu{\l}owicz, Adam},
 title		= {Categorical and Algebraic Aspects of {Martin-L\"of}
	Type Theory},
 journal	= {Studia Logica},
 volume		= 48,
 year		= 1989,
 pages		= {299--318}}


@book{OdifreddiP:clart,
 author		= {Odifreddi, Piergiorgio},
 title		= {Classical Recursion Theory:
	the Theory of Functions and Sets of Natural Numbers},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 number		= 125,
 year		= 1989,
 isbn		= 0444872957}


@book{OdifreddiP:logcs,
 title		= {Logic and Computer Science},
 editor		= {Odifreddi, Piergiorgio},
 booktitle	= {Logic and Computer Science},
 publisher	= {Academic Press},
 series		= {APIC Studies in Data Processing},
 number		= 31,
 year		= 1990}


@article{OsiusG:catstc,
 author		= {Osius, Gerhard},
 title		= {Categorical Set Theory: a Characterisation of the Category of Sets},
 journal	= {Journal of Pure and Applied Algebra},
 volume		= 4,
 year		= 1974,
 pages		= {79--119},
 review		= {MR 51/643}}


@techreport{ParkDMR:ycslcm,
 author		= {Park, David},
 title		= {The {$\mathsf{Y}$}-combinator in {S}cott's
	Lambda-calculus Models},
 institution	= {Department of Computer Science, University of Warwick},
 type		= {Research Report},
 number		= {CS-RR-013},
 month		= {June},
 year		= 1976,
 note		= {Revised, 1978},
 url		= {http://www.dcs.warwick.ac.uk/pub/reports/rr/013.html}}


@article{PasynkovBA:partp,
 author		= {Pasynkov, Boris},
 title		= {Partial Topological Products},
 journal	= {Transactions of the Moscow Mathematical Society},
 volume		= 13,
 year		= 1965,
 pages		= {153--271}}


@book{PaulsonLC:logcip,
 author		= {Paulson, Lawrence},
 title		= {Logic and Computation:
	Interactive proof with {C}ambridge {LCF}},
 publisher	= {Cambridge University Press},
 series		= {Cambridge Tracts in Theoretical Computer Science},
 number		= 2,
 year		= 1987,
 isbn		= 0521346320}


@book{PaulsonLC:mlwp,
 author		= {Paulson, Lawrence},
 title		= {{ML} for the Working Programmer},
 publisher	= {Cambridge University Press},
 year		= 1991,
 note		= {Second edition, 1996},
 isbn		= 0521390222}


@incollection{PaulsonLC:destp,
 author		= {Paulson, Lawrence},
 title		= {Designing a Theorem Prover},
 editor		= {Abramsky, Samson and others},
 booktitle	= {Handbook of Logic in Computer Science},
 publisher	= {Oxford University Press},
 year		= 1992,
 pages		= {415--475}}


@book{PaulsonLC:isagtp,
 author		= {Paulson, Lawrence},
 title		= {Isabelle: a Generic Theorem Prover},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Computer Science},
 number		= 828,
 year		= 1994,
 isbn		= {3-540-58244-4, 0-387-58244-4}}


@phdthesis{PavlovicD:phd,
 author		= {Pavlovi{\'c}, Du{\v s}ko},
 title		= {Predicates and Fibrations},
 school		= {Rijksuniversiteit Utrecht},
 year		= 1990}


@inproceedings{PavlovicD:conp,
 author		= {Pavlovi{\'c}, Du{\v s}ko},
 title		= {Constructions and Predicates},
 pages		= {173--197},
 crossref	= {PittD:cattcs4}}


@book{PeanoG:aripnm,
 author		= {Peano, Giuseppe},
 title		= {Arithmetices Principia, Nova Methodo Exposita},
 publisher	= {Fratres Bocca},
 address	= {Turin},
 year		= 1889,
 note		= {English translation,
	``The Principles of Arithmetic, presented by a new method\tuck,''
	in \cite{vanHeijenoortJ:frofgs}, pages 20--55}}


@book{PeanoG:selwgp,
 author		= {Peano, Giuseppe},
 title		= {Selected Works of {G}iuseppe {P}eano},
 publisher	= {Toronto University Press},
 year		= 1973,
 note		= {Translated and edited by Hubert Kennedy}}


@book{PeirceCS:colp,
 author		= {Peirce, Charles Sanders},
 title		= {Collected Papers},
 publisher	= {Harvard University Press},
 year		= 1933,
 note		= {Edited by Charles Hartshorne and Paul Weiss}}


@book{PierceBC:basctc,
 author		= {Pierce, Benjamin},
 title		= {Basic Category Theory for Computer Scientists},
 booktitle	= {Basic Category Theory for Computer Scientists},
 publisher	= {MIT Press},
 series		= {Foundations of Computing},
 year		= 1991,
 isbn		= {0-262-66071-7},
 lccn		= {QA76.9.M35 P54 1991}}


@proceedings{PittD:cattcs3,
 title		= {Category Theory in Computer Science {III}},
 editor		= {Pitt, David and Rydeheard, David and Dybjer, Peter and Pitts, Andrew and Poign{\'e}, Axel},
 booktitle	= {Category Theory in Computer Science {III}},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Computer Science},
 number		= 389,
 year		= 1989,
 isbn		= {038751662X}}


@proceedings{PittD:cattcs4,
 title		= {Category Theory in Computer Science {IV}},
 editor		= {Pitt, David and Curien, Pierre-Louis and Abramsky, Samson and Pitts, Andrew and Poign{\'e}, Axel and Rydeheard, David},
 booktitle	= {Category Theory in Computer Science {IV}},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Computer Science},
 number		= 530,
 year		= 1991,
 isbn		= {354054495X}}


@inproceedings{PittsAM:nonptc,
 author		= {Pitts, Andrew},
 title		= {Non-trivial Power Types can't be
	Subtypes of Polymorphic Types},
 booktitle	= {Logic in Computer Science {IV}},
 publisher	= {IEEE Computer Society Press},
 year		= 1989,
 pages		= {6--13}}


@article{PittsAM:notrpl,
 author		= {Pitts, Andrew and Taylor, Paul},
 title		= {A Note on {Russell's} {Paradox} in Locally Cartesian Closed
	Categories},
 journal	= {Studia Logica},
 volume		= 48,
 year		= 1989,
 pages		= {377--387}}


@techreport{PittsAM:catl,
 author		= {Pitts, Andrew},
 title		= {Categorical Logic},
 institution	= {University of Cambridge Computer Laboratory},
 type		= {Technical Report},
 number		= 367,
 month		= may,
 year		= 1995}


@proceedings{PittsAM:semlc,
 title		= {Semantics and Logics of Computation},
 editor		= {Pitts, Andrew and Dybjer, Peter},
 booktitle	= {Semantics and Logics of Computation},
 publisher	= {Cambridge University Press},
 series		= {Publications of the {N}ewton {I}nstitute},
 year		= 1997}


@article{PlotkinGD:lcfcpl,
 author		= {Plotkin, Gordon},
 title		= {{LCF} considered as a Programming Language},
 journal	= {Theoretical Computer Science},
 volume		= 5,
 year		= 1977,
 pages		= {223--255}}


@unpublished{PlotkinGD:posgln,
 author		= {Plotkin, Gordon},
 title		= {Domain Theory},
 year		= 1981,
 note		= {Post-graduate lecture notes, known as the Pisa Notes;
	\texttt{ftp.lfcs.ed.ac.uk}}}


@book{PohlersW:proti,
 author		= {Pohlers, Wolfram},
 title		= {Proof Theory: an Introduction},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 1407,
 year		= 1989}


@book{PolyaG:howsi,
 author		= {Polya, George},
 title		= {How to Solve It: a New Aspect of Mathematical Method},
 publisher	= {Princeton University Press},
 year		= 1945,
 note		= {Re-published by Penguin, 1990}}


@book{PrawitzD:natdpt,
 author		= {Prawitz, Dag},
 title		= {Natural Deduction: a Proof-Theoretical Study},
 publisher	= {Almquist and Wiskell},
 series		= {Stockholm Studies in Philosophy},
 number		= 3,
 year		= 1965}


@article{PrawitzD:meap,
 author		= {Prawitz, Dag},
 title		= {Meanings and Proofs: on the Conflict between Classical and
	Intutitionistic Logic},
 journal	= {Theoria},
 volume		= 43,
 year		= 1977,
 pages		= {2--40}}


@book{QuineWVO:woro,
 author		= {Quine, Willard van Orman},
 title		= {Word and Object},
 publisher	= {MIT Press},
 series		= {Studies in Communication},
 year		= 1960,
 isbn		= 0262170019}


@book{RamseyF:foum,
 author		= {Ramsey, Frank},
 title		= {Foundations of Mathematics},
 publisher	= {Kegan Paul},
 address	= {London},
 year		= 1931}


@book{RasiowaH:matm,
 author		= {Rasiowa, Helena and Sikorski, Roman},
 title		= {The Mathematics of Metamathematics},
 publisher	= {Polish Scientific Publishers},
 series		= {Monogrfie Matematyczne},
 number		= 41,
 year		= 1963,
 review		= {MR 29/1149}}


@book{RasiowaH:alganc,
 author		= {Rasiowa, Helena},
 title		= {An Algebraic Approach to Non-classical Logics},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 number		= 78,
 year		= 1974}


@inproceedings{ReynoldsJC:typapp,
 author		= {Reynolds, John},
 title		= {Types, Abstraction and Parametric Polymorphism},
 editor		= {Mason, Richard},
 booktitle	= {Information Processing},
 publisher	= {North-Holland},
 year		= 1983,
 pages		= {513--524}}


@inproceedings{ReynoldsJC:polst,
 author		= {Reynolds, John},
 title		= {Polymorhism is not Set-Theoretic},
 editor		= {Kahn, Gilles and MacQueen, David and Plotkin, Gordon},
 booktitle	= {Semantics of Data Types},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Computer Science},
 number		= 173,
 year		= 1984,
 pages		= {145--156}}


@article{ReynoldsJC:funepl,
 author		= {Reynolds, John and Plotkin, Gordon},
 title		= {On Functors Expressible in the Polymorphic Lambda Calculus},
 journal	= {Information and Computation},
 volume		= 105,
 year		= 1993,
 pages		= {1--29}}


@book{ReynoldsJC:thepl,
 author		= {Reynolds, John},
 title		= {Theories of Programming Languages},
 year		= 1998,
 publisher	= {Cambridge University Press},
 isbn		= {0 521 59414 6},
 callno		= {QA76.7.R495}}


@article{RiceHG:recreo,
 author		= {Rice, Gordon},
 title		= {Recursive and Recursively Enumerable Orders},
 journal	= {Transactions of the American Mathematical Society},
 volume		= 83,
 year		= 1956,
 pages		= 277}


@book{RobinsonA:nonsa,
 author		= {Robinson, Abraham},
 title		= {Non-standard Analysis},
 publisher	= {North-Holland},
 address	= {Amsterdam},
 series		= {Studies in Logic and the Foundations of Mathematics},
 year		= 1966}


@book{RobinsonDJ:coutg,
 author		= {Robinson, Derek},
 title		= {A Course in the Theory of Groups},
 publisher	= {Springer-Verlag},
 series		= {Graduate Texts in Mathematics},
 number		= 80,
 year		= 1982,
 note		= {Second edition, 1996},
 isbn		= 0387906002}


@article{RobinsonE:catpm,
 author		= {Robinson, Edmund and Rosolini, Giuseppe},
 title		= {Categories of Partial Maps},
 journal	= {Information and Computation},
 volume		= 79,
 year		= 1988,
 pages		= {95--130}}


@book{RussellBAW:primat,
 author		= {Russell, Bertrand},
 title		= {The Principles of Mathematics},
 publisher	= {Cambridge University Press},
 year		= 1903}


@article{RussellBAW:matlbt,
 author		= {Russell, Bertrand},
 title		= {Mathematical Logic based on the Theory of Types},
 journal	= {American Journal of Mathematics},
 volume		= 30,
 year		= 1908,
 pages		= {222--262},
 note		= {Reprinted in \cite{vanHeijenoortJ:frofgs}, pages 150--182}}


@book{RussellBAW:prim,
 author		= {Russell, Bertrand and Whitehead, Alfred North},
 title		= {Principia Mathematica},
 publisher	= {Cambridge University Press},
 year		= {1910--13}}


@book{RydeheardDE:comct,
 author		= {Rydeheard, David and Burstall, Rod},
 title		= {Computational Category Theory},
 publisher	= {Prentice-Hall},
 seriestitle	= {International Series in Computer Science},
 year		= 1988,
 isbn		= {0-13-162736-8},
 libcongr	= {88-4232}}


@article{SamuelP:unimft,
 author		= {Samuel, Pierre},
 title		= {On Universal Mappings and Free Topological Groups},
 journal	= {Bulletin of the American Mathematical Society},
 volume		= 54,
 year		= 1948,
 pages		= {591--598}}


@incollection{ScedrovA:notfsf,
 author		= {Scedrov, Andre and Scott, Philip},
 title		= {A Note on the {F}riedman Slash and {F}reyd Covers},
 year		= 1982,
 pages		= {443--452},
 crossref	= {TroelstraAS:lejbcs}}


@article{SchalkA:domaap,
 author		= {Schalk, Andrea},
 title		= {Domains arising as Algebras for Power Space Constructions},
 journal	= {Journal of Pure and Applied Algebra},
 year		= 1993}


@book{SchoenfieldJR:matl,
 author		= {Schoenfield, Joseph},
 title		= {Mathematical Logic},
 publisher	= {Addison-Wesley},
 year		= 1967}


@incollection{ScottDS:morax,
 author		= {Scott, Dana},
 title		= {More on the Axiom of Extensionality},
 pages		= {115--139},
 note		= {},
 crossref	= {BarHillelY:essfm}}


@inproceedings{ScottDS:conv,
 author		= {Scott, Dana},
 title		= {Constructive Validity},
 editor		= {Laudet, Michel and Lacombe, D. and Nolin, L. and Sch{\"u}tzenberger, M.},
 booktitle	= {Automatic Demonstration},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 125,
 year		= 1970,
 pages		= {237--275}}


@incollection{ScottDS:outmtc,
 author		= {Scott, Dana},
 title		= {Outline of a Mathematical Theory of Computation},
 booktitle	= {Information Sciences and Systems},
 publisher	= {Princeton University Press},
 year		= 1970,
 pages		= {169--176}}


@article{ScottDS:dattl,
 author		= {Scott, Dana},
 title		= {Data Types as Lattices},
 journal	= {SIAM Journal on Computing},
 volume		= 5,
 year		= 1976,
 pages		= {522--587}}


@inproceedings{ScottDS:ideeil,
 author		= {Scott, Dana},
 title		= {Identity and Existence in Intuitionistic Logic},
 pages		= {660--696},
 crossref	= {FourmanMP:apps}}


@book{Seebach:cout,
 author		= {Seebach, J. Arthur and Steen, Lynn Arthur},
 title		= {Counterexamples in Topology},
 publisher	= {Holt, Rinehart and Winston},
 year		= 1970,
 note		= {Republished by Springer-Verlag, 1978 and by
	Dover, 1995}}


@article{SeelyRAG:locccc,
 author		= {Seely, Robert},
 title		= {Locally Cartesian Closed Categories and Type Theory},
 journal	= {Mathematical Proceedings of the Cambridge Philosophical Society},
 volume		= 95,
 year		= 1984,
 pages		= {33--48}}


@article{SeelyRAG:catsho,
 author		= {Seely, Robert},
 title		= {Categorical Semantics for Higher Order Polymorphic
	Lambda Calclus},
 journal	= {Journal of Symbolic Logic},
 volume		= 52,
 year		= 1987,
 pages		= {969--989}}


@inproceedings{SeelyRAG:linlac,
 author		= {Seely, Robert},
 title		= {Linear Logic, {$*$}-Autonomous Categories and Cofree Algebras},
 pages		= {371--382},
 crossref	= {GrayJW:catcsl},
 urlps		= {ftp://ftp.math.mcgill.ca/pub/rags/nets/llsac.ps.gz}}


@book{SerreJP:replgf,
 author		= {Serre, Jean-Pierre},
 title		= {Rep\'esentations Lin\'eaires des Groupes Finis},
 publisher	= {Hermann},
 year		= 1971,
 note		= {English translation, ``Linear representations of finite groups''
	by Leonard Scott, Springer-Verlag, Graduate Texts in Mathematics 42,
	1976, reprinted 1986}}


@book{ShapiroS:fouwf,
 author		= {Shapiro, Stewart},
 title		= {Foundations without Foundationalism:
	a Case for Second-order Logic},
 publisher	= {Oxford University Press},
 series		= {Logic Guides},
 number		= 17,
 year		= 1991}


@incollection{SkolemT:bemabm,
 author		= {Skolem, Thoralf},
 title		= {Einige {B}emerkungen zur axiomatischen {B}egr{\"u}ndung der
	{M}engenlehre},
 booktitle	= {Skandinaviska matematikenkongressen},
 publisher	= {Akademiska Bokhandeln},
 year		= 1922,
 pages		= {217--232},
 note		= {English translation, ``Some Remarks on Axiomatized
	Set Theory'' in \cite{vanHeijenoortJ:frofgs}, pages
	290--301},
 city		= {Helsinki}}


@book{SkolemT:selwl,
 author		= {Skolem, Thoralf},
 title		= {Selected Works in Logic},
 publisher	= {Universitetsforlaget},
 address	= {Oslo},
 year		= 1970,
 note		= {Edited by Jens Erik Fenstad}}


@article{SteenrodN:concts,
 author		= {Steenrod, Norman},
 title		= {A Convenient Category of Topological Spaces},
 journal	= {Michigan Mathematics Journal},
 volume		= 14,
 year		= 1967,
 pages		= {133--152},
 comment	= {Compactly generated or K-spaces form a CCC}}


@article{StoneM:apptbr,
 author		= {Stone, Marshall},
 title		= {Applications of the Theory of {B}oolean Rings to General Topology},
 journal	= {Transactions of the American Mathematical Society},
 volume		= 41,
 year		= 1937,
 pages		= {375--481}}


@article{StreetRH:comff,
 author		= {Street, Ross and Walters, Robert},
 title		= {The Comprehensive Factorization of a Functor},
 journal	= {Bulletin of the American Mathematical Society},
 volume		= 79,
 year		= 1973,
 pages		= {936--941},
 review		= {MR49#10753}}


@article{StreetRH:cosic,
 author		= {Street, Ross},
 title		= {Cosmoi of Internal Categories},
 journal	= {Transactions of the American Mathematical Society},
 volume		= 258,
 year		= 1980,
 pages		= {271--318}}


@book{StreicherT:phd,
 author		= {Streicher, Thomas},
 title		= {Semantics of Type Theory:
	Correctness and Completeness of a Categorical Semantics
	of the Calculus of Constructions},
 publisher	= {Birkh{\"a}user},
 series		= {Progress in Theoretical Computer Science},
 year		= 1991,
 note		= {His 1988 Passau Ph.D. thesis},
 isbn		= 3764335947}


@book{StruikDJ:soubm,
 author		= {Struik, Dirk},
 title		= {A Source Book in Mathematics, 1200--1800},
 publisher	= {Harvard University Press},
 year		= 1969}


@book{StyazhkinNI:hismll,
 author		= {Styazhkin, N. I.},
 title		= {History of Mathematical Logic from {L}eibniz to {P}eano},
 publisher	= {MIT Press},
 year		= 1969,
 note		= {Translated from Russian, originally published by
	Nauka, Moscow, 1964},
 isbn		= {0 262 19057 5}}


@inproceedings{TaitW:reaits,
 author		= {Tait, William},
 title		= {A Realizability Interpretation of the Theory of Species},
 editor		= {Parik, R.},
 booktitle	= {Logic Colloquium},
 publisher	= {Springer-Verlag},
 year		= 1975,
 pages		= {240--251}}


@book{TakeutiG:prot,
 author		= {Takeuti, Gaisi},
 title		= {Proof Theory},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 number		= 81,
 year		= 1975,
 note		= {Second edition, 1987},
 isbn		= {0-444-10492-5},
 callno		= {510.1 T13p}}


@book{TarskiA:logsm,
 author		= {Tarski, Alfred},
 title		= {Logic, Semantics, Metamathematics},
 publisher	= {Oxford University Press},
 year		= 1956,
 note		= {Edited by J. H. Woodger}}


@inproceedings{TaylorP:intccd,
 author		= {Taylor, Paul},
 title		= {Internal Completeness of Categories of Domains},
 editor		= {Pitt, David},
 booktitle	= {Category Theory and Computer Programming},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Computer Science},
 number		= 240,
 year		= 1986,
 pages		= {449--465},
 isbn		= 3540171622}


@phdthesis{TaylorP:phd,
 author		= {Taylor, Paul},
 title		= {Recursive Domains, Indexed Category Theory and Polymorphism},
 school		= {Cambridge University},
 year		= 1986}


@unpublished{TaylorP:hombsd,
 author		= {Taylor, Paul},
 title		= {Homomorphisms, Bilimits and Saturated Domains ---
	some very basic domain theory},
 year		= 1987,
 pages		= 26,
 note		= {\texttt{ftp.dcs.qmw.ac.uk}}}


@unpublished{TaylorP:trafsf,
 author		= {Taylor, Paul},
 title		= {The Trace Factorisation of Stable Functors},
 year		= 1988}


@inproceedings{TaylorP:quadgl,
 author		= {Taylor, Paul},
 title		= {Quantitative Domains, Groupoids and Linear Logic},
 pages		= {155--181},
 crossref	= {PittD:cattcs3}}


@article{TaylorP:algasd,
 author		= {Taylor, Paul},
 title		= {An Algebraic Approach to Stable Domains},
 journal	= {Journal of Pure and Applied Algebra},
 publisher	= {North-Holland},
 volume		= 64,
 year		= 1990,
 pages		= {171--203}}


@inproceedings{TaylorP:fixpps,
 author		= {Taylor, Paul},
 title		= {The Fixed Point Property in Synthetic Domain Theory},
 editor		= {Kahn, Gilles},
 booktitle	= {Logic in Computer Science 6},
 publisher	= {IEEE Computer Society Press},
 year		= 1991,
 pages		= {152--160}}


@article{TaylorP:intso,
 author		= {Taylor, Paul},
 title		= {Intuitionistic Sets and Ordinals},
 journal	= {Journal of Symbolic Logic},
 volume		= 61,
 year		= 1996,
 pages		= {705--744}}


@unpublished{TaylorP:towuti,
 author		= {Taylor, Paul},
 title		= {On the General Recursion Theorem},
 year		= 1996}


@unpublished{TaylorP:abssd1,
 author		= {Taylor, Paul},
 title		= {An Abstract Stone Duality,~{I}:
	Geometric and Higher Order Logic},
 note		= {In preparation},
 year		= 1998}


@book{TennentRD:pripl,
 author		= {Tennent, Robert},
 title		= {Principles of Programming Languages},
 publisher	= {Prentice-Hall},
 isbn		= {0 13 7098731},
 year		= 1981}


@book{TennentRD:sempl,
 author		= {Tennent, Robert},
 title		= {Semantics of Programming Languages},
 publisher	= {Prentice-Hall},
 series		= {International Series in Computer Science},
 isbn		= {0 13 805 607 2},
 year		= 1991,
 callno		= {QA76.7.T473}}


@incollection{TierneyM:shetch,
 author		= {Tierney, Miles},
 title		= {Sheaf Theory and the Continuum Hypothesis},
 pages		= {13--42},
 review		= {MR 51/10088},
 crossref	= {LawvereFW:topagl}}


@book{TroelstraAS:prii,
 author		= {Troelstra, Anne Sjerp},
 title		= {Principles of Intuitionism},
 publisher	= {Springer-Verlag},
 series		= {Lecture Notes in Mathematics},
 number		= 95,
 year		= 1969}


@book{TroelstraAS:chosci,
 author		= {Troelstra, Anne Sjerp},
 title		= {Choice Sequences: a Chapter of Inttuitionistic Mathematics},
 publisher	= {Oxford University Press},
 series		= {Logic Guides},
 year		= 1977}


@proceedings{TroelstraAS:lejbcs,
 title		= {L.~E.~J.~Brouwer Centenary Symposium},
 editor		= {Troelstra, Anne Sjerp and van Dalen, Dirk},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 number		= 110,
 year		= 1982,
 isbn		= 0444864946}


@book{TroelstraAS:conmi,
 author		= {Troelstra, Anne Sjerp and van Dalen, Dirk},
 title		= {Constructivism in Mathematics, an Introduction},
 publisher	= {North-Holland},
 series		= {Studies in Logic and the Foundations of Mathematics},
 number		= {121 and 123},
 year		= 1988,
 isbn		= {0444702660 0444703586}}


@book{TroelstraAS:baspt,
 author		= {Troelstra, Anne Sjerp and Schwichtenberg, Helmut},
 title		= {Basic Proof Theory},
 publisher	= {Cambridge University Press},
 series		= {Cambridge Tracts in Theoretical Computer Science},
 number		= 43,
 year		= 1996}


@article{TuringAM:comnae,
 author		= {Turing, Alan},
 title		= {On Computable Numbers with an Application to the
	{E}ntscheidungsproblem},
 journal	= {Proceedings of the London Mathematical Society (2)},
 volume		= 42,
 year		= 1935,
 pages		= {230--265}}


@book{vanDalenD:logs,
 author		= {van Dalen, Dirk},
 title		= {Logic and Structure},
 publisher	= {Springer-Verlag},
 series		= {Universitext},
 year		= 1980,
 note		= {Second edition, 1983},
 isbn		= {3 540 12831 X},
 ams_subj	= {03-01}}


@book{vanderWaerdenBL:moda,
 author		= {van der Waerden, Bartel},
 title		= {Moderne Algebra},
 publisher	= {Ungar},
 year		= 1931,
 note		= {Fifth edition, Springer-Verlag, 1960;
	English translation by Fred Blum and John Schulenberger,
	``Algebra\tuck,'' Springer-Verlag, 1971},
 isbn		= 0804449481}


@book{vanHeijenoortJ:frofgs,
 title		= {From {F}rege to {G}{\"o}del:
	a Source Book in Mathematical Logic, 1879--1931},
 editor		= {van Heijenoort, Jan},
 publisher	= {Harvard University Press},
 year		= 1967,
 note		= {Reprinted 1971, 1976}}


@book{VickersSJ:topvl,
 author		= {Vickers, Steven},
 title		= {Topology via Logic},
 publisher	= {Cambridge University Press},
 series		= {Cambridge Tracts in Theoretical Computer Science},
 number		= 5,
 year		= 1988,
 isbn		= 0521360625}


@book{vonNeumannJ:colw,
 author		= {von Neumann, John},
 title		= {Collected Works},
 publisher	= {Pergamon Press},
 year		= 1961,
 note		= {Edited by A. H. Taub}}


@book{WebbJC:mecmm,
 author		= {Webb, Judson Chambers},
 title		= {Mechanism, Mentalism and Metamathematics:
	an Essay on Finitism},
 publisher	= {Reidel},
 series		= {Synthese Library},
 number		= 137,
 year		= 1980,
 isbn		= 9027710465}


@book{WellsC:hanmd,
 author		= {Wells, Charles},
 title		= {The Handbook of Mathematical Discourse},
 note		= {\texttt{http://www-math.cwru.edu/~cfw2/abouthbk.htm}},
 year		= 1996}


@article{WeylH:con,
 author		= {Weyl, Hermann},
 title		= {Der {C}irculus vitiosus in der heutigen
	{B}egr{\"u}ndung der {A}nalysis},
 journal	= {Jahrbericht der deutschen {M}atematiker-{V}ereinigung},
 volume		= 28,
 year		= 1919,
 pages		= {85--92},
 note		= {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},
 isbn		= {0-486-67982-9}}


@book{WeylH:gesa,
 author		= {Weyl, Hermann},
 title		= {Gesammelte {A}bhandlungen},
 publisher	= {Springer-Verlag},
 year		= 1968,
 note		= {Edited by K. Chandrasekharan}}


@book{ZariskiO:coma,
 author		= {Zariski, Oscar and Samuel, Pierre},
 title		= {Commutative Algebra},
 publisher	= {Van Nostrand},
 year		= 1958,
 note		= {Reprinted by Springer-Verlag, Graduate Texts in
	Mathematics, number 28--9, 1975},
 isbn		= {0-387-90171-X}}


@article{ZermeloE:proesw,
 author		= {Zermelo, Ernst},
 title		= {Neuer {B}eweis f{\"u}r die {M\"o}glichkeit einer {W}ohlordnung},
 journal	= {Mathematische Annalen},
 volume		= 65,
 year		= 1908,
 pages		= {107--128},
 note		= {English translation, ``New proof that every set can be well ordered''
	in \cite{vanHeijenoortJ:frofgs}, pages 183--198}}


@article{ZermeloE:untgm,
 author		= {Zermelo, Ernst},
 title		= {Untersuchungen {\"u}ber die {G}rundlagen
	der {M}engenlehre~{I}},
 journal	= {Mathematische Annalen},
 volume		= 65,
 year		= 1908,
 pages		= {261--281},
 note		= {English translation, ``Investigations in the
	foundations of set theory''
	in \cite{vanHeijenoortJ:frofgs}, pages 199--215}}