Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% -*- coding: raw-text -*-
% My bibliography for Categorical Semantics & Related Stuff
% (find-angg "LATEX/filters.bib")
% (find-angg "LUA/bibtex.lua")
% ftp://ftp.math.mcgill.ca/pub/rags/SeelyRAG.bib
% ftp://ftp.imf.au.dk/pub/kock/KockA.bib
% (find-sftpfile  "ftp://ftp.cs.cmu.edu/user/jcr/ReynoldsJC.bib")
% (find-shttpfile "hypatia.dcs.qmw.ac.uk/author/FreydPJ/bilbio.bib.html")
% (find-es "tex" "bibtex")
% (find-man "1 bibtex")
% (find-efunction 'bibtex-mode)
% (describe-bindings "\C-c\C-e")

% (find-efunction 'bibtex-Book)
% (find-efunction 'bibtex-entry)
% (find-efile "textmodes/bibtex.el" "(easy-menu-define\n bibtex-edit-menu")
% (find-efile "textmodes/bibtex.el" "(easy-menu-define\n bibtex-entry-menu")

% «test»  (to ".test")
% (find-angg "LATEX/catsembibtest.tex")
% (find-angg "LATEX/filters.bib")
% (find-angg ".zshrc" "makebbl")
% (find-angg ".zshrc" "makebblcites")
% (find-zsh "cat catsem.bib             | makebblcites")
% (find-zsh "cat catsem.bib filters.bib | makebblcites")
% (find-zsh "makebbl catsem.bbl catsem,filters; latex tmpbib.tex")
% (find-zsh "makebbl catsem.bbl catsem,filters; pdflatex tmpbib.tex")
% (find-dvipage "tmpbib.dvi" 1)
% (find-pdfpage-pdftotext "tmpbib.pdf")
% (find-fline "~/LATEX/catsem.bbl")
% (find-LATEX "tmpbib.tex")


% «.test»			(to "test")
% «.bib-Antipodes»		(to "bib-Antipodes")
% «.bib-Automath»		(to "bib-Automath")
% «.bib-Awodey»			(to "bib-Awodey")
% «.bib-BarbBera»		(to "bib-BarbBera")
% «.bib-Barendregt»		(to "bib-Barendregt")
% «.bib-BarrWells»		(to "bib-BarrWells")
% «.bib-Beck»			(to "bib-Beck")
% «.bib-BellLST»		(to "bib-BellLST")
% «.bib-BellSIA»		(to "bib-BellSIA")
% «.bib-Benabou»		(to "bib-Benabou")
% «.bib-Bentley»		(to "bib-Bentley")
% «.bib-Bernardy»		(to "bib-Bernardy")
% «.bib-Bootstrapping»		(to "bib-Bootstrapping")
% «.bib-BorceuxIII»		(to "bib-BorceuxIII")
% «.bib-Byers»			(to "bib-Byers")
% «.bib-CarnielliEpstein»	(to "bib-CarnielliEpstein")
% «.bib-Coq»			(to "bib-Coq")
% «.bib-Corfield»		(to "bib-Corfield")
% «.bib-DaveyPriestley»		(to "bib-DaveyPriestley")
% «.bib-Eilenberg»		(to "bib-Eilenberg")
% «.bib-Fitting»		(to "bib-Fitting")
% «.bib-Fourman»		(to "bib-Fourman")
% «.bib-Freyd76»		(to "bib-Freyd76")
% «.bib-FreydScedrov»		(to "bib-FreydScedrov")
% «.bib-Fritz»			(to "bib-Fritz")
% «.bib-GLT»			(to "bib-GLT")
% «.bib-GeuversPhD»		(to "bib-GeuversPhD")
% «.bib-GeuversSN»		(to "bib-GeuversSN")
% «.bib-Goedel»			(to "bib-Goedel")
% «.bib-Gratzer»		(to "bib-Gratzer")
% «.bib-HellerTierney»		(to "bib-HellerTierney")
% «.bib-HylandPitts»		(to "bib-HylandPitts")
% «.bib-Jacobs»			(to "bib-Jacobs")
% «.bib-Jamnik»			(to "bib-Jamnik")
% «.bib-Johnstone»		(to "bib-Johnstone")
% «.bib-JoyalStreet»		(to "bib-JoyalStreet")
% «.bib-Kamareddine»		(to "bib-Kamareddine")
% «.bib-KellyLack»		(to "bib-KellyLack")
% «.bib-Kock77»			(to "bib-Kock77")
% «.bib-Kock81»			(to "bib-Kock81")
% «.bib-Kromer»			(to "bib-Kromer")
% «.bib-LambekScott»		(to "bib-LambekScott")
% «.bib-LangAlgebra»		(to "bib-LangAlgebra")
% «.bib-Lavendhomme»		(to "bib-Lavendhomme")
% «.bib-Lawvere80»		(to "bib-Lawvere80")
% «.bib-LawvereAdjBicat»	(to "bib-LawvereAdjBicat")
% «.bib-LawvereAdjFo»		(to "bib-LawvereAdjFo")
% «.bib-LawvereEqHyp»		(to "bib-LawvereEqHyp")
% «.bib-LawvereSchanuel»	(to "bib-LawvereSchanuel")
% «.bib-LawvereThesis»		(to "bib-LawvereThesis")
% «.bib-Luo»			(to "bib-Luo")
% «.bib-Macbeth»		(to "bib-Macbeth")
% «.bib-MacLane»		(to "bib-MacLane")
% «.bib-MacLaneMoerdijk»	(to "bib-MacLaneMoerdijk")
% «.bib-MartinLof84»		(to "bib-MartinLof84")
% «.bib-McLarty»		(to "bib-McLarty")
% «.bib-ModalHandbook»		(to "bib-ModalHandbook")
% «.bib-MoeRey»			(to "bib-MoeRey")
% «.bib-Ochs»			(to "bib-Ochs")
% «.bib-Pavlovic»		(to "bib-Pavlovic")
% «.bib-Phoa»			(to "bib-Phoa")
% «.bib-Pitts»			(to "bib-Pitts")
% «.bib-Prawitz65»		(to "bib-Prawitz65")
% «.bib-PrawitzIRPF»		(to "bib-PrawitzIRPF")
% «.bib-Reyes»			(to "bib-Reyes")
% «.bib-Reynolds»		(to "bib-Reynolds")
% «.bib-Schalk»			(to "bib-Schalk")
% «.bib-SeelyBeck»		(to "bib-SeelyBeck")
% «.bib-SeelyCartDiff»		(to "bib-SeelyCartDiff")
% «.bib-SeelyDiff»		(to "bib-SeelyDiff")
% «.bib-SeelyLCCC»		(to "bib-SeelyLCCC")
% «.bib-SeelyPLC»		(to "bib-SeelyPLC")
% «.bib-SmithGalois»		(to "bib-SmithGalois")
% «.bib-Simmons»		(to "bib-Simmons")
% «.bib-Streicher»		(to "bib-Streicher")
% «.bib-Taylor»			(to "bib-Taylor")
% «.bib-WadlerGR»		(to "bib-WadlerGR")
% «.bib-WadlerTfF»		(to "bib-WadlerTfF")
%
% «.bib-LuaGems»		(to "bib-LuaGems")
%
% «.diagrams»			(to "diagrams")


% http://www.cl.cam.ac.uk/~amp12/bib/PittsAM.bib

% «bib-Antipodes»  (to ".bib-Antipodes")
% (find-LATEX "filters.bib" "antipodes")

% «bib-Automath»  (to ".bib-Automath")
% (find-books "__logic/__logic.el" "automath")
@Book{Automath,
  editor = 	 {R. P. Nederpelt and J. H. Geuvers and R. C. de Vrijer},
  title = 	 {Selected Papers on Automath},
  publisher = 	 {North-Holland},
  year = 	 {1994},
}

% «bib-Awodey»  (to ".bib-Awodey")
% (find-books "__cats/__cats.el" "awodey")
%   OUP -> Clarendon
@Book{Awodey,
  author =	 {S. Awodey},
  title = 	 {Category Theory},
  publisher = 	 {Oxford University Press},
  year = 	 {2006},
}

% «bib-BarbBera»  (to ".bib-BarbBera")
% F. Barbanera and S. Berardi. Proof-irrelevance out of excluded-middle
% and choice in the calculus of constructions. Journal of Functional
% Programming, 6(3):519-525, May 1996.
%
@Article{BarbBera,
  author = 	 {F. Barbanera and S. Berardi},
  title =        {Proof-irrelevance out of excluded-middle and choice
		  in the calculus of constructions},
  journal = 	 {Journal of Functional Programming},
  year = 	 {1996},
  volume =	 {6},
  number =	 {3},
  pages =	 {519--525},
  month =	 {may},
}

% «bib-Barendregt»  (to ".bib-Barendregt")
% H. Barendregt. Lambda Calculi with Types, Handbook of Logic in
% Computer Science, Oxford University Press, Vol. 2, pp 117--309, 1992.
%
@InBook{Barendregt,
  author =	 {H. Barendregt},
  title = 	 {Handbook of Logic in Computer Science},
  chapter = 	 {Lambda Calculi with Types},
  publisher = 	 {Oxford University Press},
  year = 	 {1992},
  volume =	 {2},
  pages =	 {117--309},
}

% «bib-BarrWells»  (to ".bib-BarrWells")
% (find-angg ".emacs.papers" "barr")
% M. Barr and Ch. Wells. Toposes, Triples and Theories. Springer,
% Berlin, 1985.
%
@Book{BarrWells,
  author =	 {M. Barr and C. Wells},
  title = 	 {Toposes, Triples and Theories},
  publisher = 	 {Springer},
  year = 	 {1985},
  note =	 {\url{http://www.tac.mta.ca/tac/reprints/articles/12/tr12abs.html}},
}

% «bib-Beck»  (to ".bib-Beck")
% (find-angg ".emacs.papers" "beck")
%
@PhdThesis{BeckPhDThesis,
  author = 	 {J. M. Beck},
  title = 	 {Triples, Algebras and Cohomology},
  school = 	 {Columbia},
  year = 	 {1967},
  note =	 {\url{http://www.tac.mta.ca/tac/reprints/articles/2/tr2abs.html}},
}

% «bib-BellLST»  (to ".bib-BellLST")
% J. L. Bell. Toposes and Local Set Theories. volume 14 of Oxford Logic
% Guides. Oxford University Press, 1988.
%
@Book{BellLST,
  author =	 {J. L. Bell},
  title = 	 {Toposes and Local Set Theories},
  publisher = 	 {Oxford University Press},
  year = 	 {1988},
  number =	 {14},
  series =	 {Oxford Logic Guides},
}

% «bib-BellSIA»  (to ".bib-BellSIA")
% (find-books "__cats/__cats.el" "bell")
@Book{BellSIA,
  author = 	 {J. L. Bell},
  title = 	 {A Primer of Infinitesimal Analysis},
  publisher = 	 {Cambridge},
  year = 	 {2008},
}



% «bib-Benabou»  (to ".bib-Benabou")
% (find-angg ".emacs.papers" "benabou")
%
@Article{Benabou,
  author = 	 {J. Bénabou},
  title =        {Fibred Categories and the Foundations of Naive Category
                  Theory},
  journal = 	 {Journal of Symbolic Logic},
  year = 	 {1985},
  volume = 	 {50},
  number = 	 {1},
  pages = 	 {10--37}
}

% «bib-Bentley»  (to ".bib-Bentley")
% (find-angg ".emacs.papers" "bentley")
% Also in "More Programming Pearls", chapter 9, 83-100
% Addison-Wesley, 1988
%
@Article{LittleLanguages,
  author = 	 {J. Bentley},
  title = 	 {Little Languages},
  journal = 	 {CACM [Fix This]},
  year = 	 {1977},
}

% «bib-Bernardy»  (to ".bib-Bernardy")
% http://www.cse.chalmers.se/~bernardy/ParDep/pardep.pdf
% http://www.cse.chalmers.se/~bernardy/#publications
%
@Article{Bernardy10,
  author = 	 {J. P. Bernardy and P. Jansson and R. Paterson},
  title = 	 {Parametricity and dependent types},
  journal = 	 {International Conference on Functional Programming},
  year = 	 {2010},
  note = 	 {\url{http://www.cse.chalmers.se/~bernardy/ParDep/pardep.pdf}},
}

% «bib-Bootstrapping»  (to ".bib-Bootstrapping")
% (to "bib-LuaGems")
% (find-TH "luaforth")
% (find-TH "miniforth-article")
% http://www.lua.org/gems/
% (find-kopkadaly4page (+ 12 319) "Index")
% (find-kopkadaly4text)
%
@InProceedings{Bootstrapping,
  crossref =     {LuaGems},
  author = 	 {E. Ochs},
  title = 	 {Bootstrapping a Forth in 40 Lines of Lua Code},
  chapter = 	 {6},
}

% «bib-BorceuxIII»  (to ".bib-BorceuxIII")
% (find-books "__cats/__cats.el" "borceux")
%
@Book{BorceuxIII,
  author =	 {F. Borceux},
  title = 	 {Handbook of Categorical Algebra III: Categories of Sheaves},
  publisher = 	 {Cambridge},
  year = 	 {1994},
  volume =	 {52},
  series =	 {Encyclopedia of Mathematics and its Applications}
}

% «bib-Byers»  (to ".bib-Byers")
% (find-books "__phil/__phil.el" "byers")
%
@Book{Byers,
  author = 	 {W. Byers},
  title = 	 {How Mathematicians Think},
  publisher = 	 {Princeton},
  year = 	 {2007},
}

% «bib-CarnielliEpstein»  (to ".bib-CarnielliEpstein")
%
@Book{CarnielliEpstein06,
  author = 	 {W. Carnielli and R. L. Epstein},
  title = 	 {Computabilidade, Funções Computáveis, Lógica e os Fundamentos da Matemática},
  publisher = 	 {Ed. UNESP},
  year = 	 {2006},
}

% «bib-Coq»  (to ".bib-Coq")
% (find-es "coq" "bertot-casteran")
% (find-books "__comp/__comp.el" "coq")
% http://books.google.com/books?id=m5w5PRj5Nj4C
%
@Book{BertotCasteran,
  author = 	 {Y. Bertot and P. Castéran},
  title = 	 {Interactive Theorem Proving and Program Development
                  - Coq'Art: The Calculus of Inductive Constructions},
  publisher = 	 {Springer},
  year = 	 {2004},
}


% «bib-Corfield»  (to ".bib-Corfield")
% (find-books "__phil/__phil.el" "corfield")
%
@Book{Corfield,
  author = 	 {D. Corfield},
  title = 	 {Towards a Philosophy of Real Mathematics},
  publisher = 	 {Cambridge},
  year = 	 {2004},
}


% «bib-DaveyPriestley» (to ".bib-DaveyPriestley")
% (find-books "__alg/__alg.el" "davey-priestley")
% isbn={9780521784511},
% lccn={2001043910},
% url={https://books.google.com.br/books?id=vVVTxeuiyvQC},
% series =  {Cambridge Mathematical Textbooks},
%
@book{DaveyPriestley,
  title =     {Introduction to Lattices and Order},
  author =    {Davey, B.A. and Priestley, H.A.},
  year =      {2002},
  publisher = {Cambridge University Press}
}



% «bib-Eilenberg»  (to ".bib-Eilenberg")
% (find-books "__cats/__cats.el" "kromer")
%
@Book{EilenbergSteenrod,
  author = 	 {S. Eilenberg and N. Steenrod},
  title = 	 {Foundations of algebraic topology},
  publisher = 	 {Princeton},
  year = 	 {1952},
}


% «bib-Fitting72» (to ".bib-Fitting")
% (find-books "__modal/__modal.el" "fitting")
% Melvin Fitting: "Tableau Methods of Proof For Modal Logics" (1972)
@Article{Fitting72,
  author = 	 {M. Fitting},
  title = 	 {Tableau Methods of Proof For Modal Logics},
  journal = 	 {Notre Dame Journal of Formal Logic},
  year = 	 {1972},
  volume = 	 {XIII},
  number = 	 {2},
  pages = 	 {237-247},
  month = 	 {April},
}




% «bib-Fourman» (to ".bib-Fourman")
% (find-books "__cats/__cats.el" "fourman")
% (find-slnm0753page         5  "Contents")
% (find-slnm0753page (+ 14 302) "Sheaves and Logic" "Fourman" "Scott")
% 
% https://link.springer.com/bookseries/304 SLNM
% https://link.springer.com/book/10.1007/BFb0061811 Applications of sheaves
% https://link.springer.com/chapter/10.1007%2FBFb0061824 Sheaves and Logic
% https://link.springer.com/chapter/10.1007%2FBFb0061824#page-1
%
@InProceedings{Fourman,
  author =    {M.P. Fourman and D.S. Scott},
  title =     {Sheaves and Logic},
  booktitle = {Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra and Analysis - Durham, july 9-21, 1977},
  pages =     {302--401},
  year =      {1979},
  number =    {753},
  editor =    {M.P. Fourman and D.J. Mulvey and D.S. Scott},
  publisher = {Springer},
  series =    {Lecture Notes in Mathematics},
}



% «bib-Freyd76»  (to ".bib-Freyd76")
% (to "bib-HellerTierney")
% (find-angg ".emacs.papers" "freyd")
% http://angg.twu.net/scans/freyd76__properties_invariant_within_equivalence_types_of_categories.pdf
% http://angg.twu.net/scans/freyd76__properties_invariant_within_equivalence_types_of_categories.djvu
%
@InProceedings{Freyd76,
  author = 	 {P. Freyd},
  title = 	 {Properties Invariant within Equivalence Types of Categories},
  booktitle =    {Algebra, Topology and Category Theory: A Collection of Papers in Honour of Samuel Eilenberg},
  pages = 	 {55--61},
  year = 	 {1976},
  editor = 	 {A. Heller and M. Tierney},
  publisher =    {Academic Press},
}


% «bib-FreydScedrov»  (to ".bib-FreydScedrov")
% (find-books "__cats/__cats.el" "freyd-scedrov")
%
@Book{FreydScedrov,
  author = 	 {P. Freyd and A. Scedrov},
  title = 	 {Categories, Allegories},
  publisher = 	 {North-Holland},
  year = 	 {1990},
}


% «bib-Fritz»  (to ".bib-Fritz")
% (find-angg ".emacs.papers" "fritz")
% (find-efile "textmodes/bibtex.el" "TechReport")
% (find-kopkadaly4page (+ 12 219) "Index")
% (find-es "tex" "bibtex")
% 
@Misc{Fritz,
  author = 	 {T. Fritz},
  title = 	 {Categories of Fractions Revisited},
  year = 	 {2008},
  howpublished = {Preprint},
  note =	 {\url{http://arxiv.org/abs/0803.2587}},
}

% «bib-GLT»  (to ".bib-GLT")
% (find-angg ".emacs.papers" "girard")
%
@Book{GLT,
  author = 	 {J.-Y. Girard and Y. Lafont and P. Taylor},
  title = 	 {Proofs and Types},
  publisher = 	 {Cambridge},
  year = 	 {1989},
}

% «bib-GeuversPhD»  (to ".bib-GeuversPhD")
% H. Geuvers. Logics and Type Systems. PhD thesis, University of
% Nijmegen, 1993.
%
@PhdThesis{GeuversPhD,
  author = 	 {H. Geuvers},
  title = 	 {Logics and Type Systems},
  school = 	 {University of Nijmegen},
  year = 	 {1993},
}

% «bib-GeuversSN»  (to ".bib-GeuversSN")
% H. Geuvers. A short and flexible proof of strong normalisation for the
% calculus of constructions. In P. Dybjer, B. Nordstrom, and J. Smith,
% editors, Proceedings of TYPES'94, volume 996 of Lecture Notes in
% Computer Science, pages 14--38. Springer-Verlag, 1995.
%
% J. H. Geuvers. A short and flexible proof of strong normalization for
% the Calculus of Constructions. In Types for Proofs and Programs, P.
% Dybjer, B. Nordström and J. Smith (eds), LNCS 996, Springer, 1994.
%
@InProceedings{GeuversSN,
  author = 	 {H. Geuvers},
  title = 	 {A short and flexible proof of strong normalisation
		  for the calculus of constructions},
  booktitle =	 {Proceedings of TYPES'94},
  pages =	 {14--38},
  year =	 {1995},
  editor =	 {P. Dybjer and B. Nordstrom and J. Smith},
  number =	 {996},
  series =	 {Lecture Notes in Computer Science},
  publisher =	 {Springer},
}


% «bib-Goedel» (to ".bib-Goedel")
% (find-books "__logic/__logic.el" "godel")
% (find-godel1page         1  "")
% (find-godel1page        18  "Contents")
% (find-godel1page (+ 27  16) "Works in the first two volumes")
% (find-godel1page (+ 27 296) "Introductory note to 1933f")
% (find-godel1page (+ 27 301) "An interpretation of the intuitionistic propositional calculus (1933f)")
%
@Book{GoedelCollWorks1,
  editor = 	 {S. Feferman},
  title =        {Kurt Gödel, Collected Works vol.1 (Publications 1929--1936)},
  publisher = 	 {Oxford},
  year = 	 {1986},
}
@InBook{Goedel1933f,
  editor = 	 {S. Feferman},
  booktitle =    {Kurt Gödel, Collected Works vol.1 (Publications 1929--1936)},
  publisher = 	 {Oxford},
  year = 	 {1986},
  author =	 {K. Goedel},
  title =        {An interpretation of the intuitionistic propositional calculus (1933f)},
  pages =        {301},
}
@InBook{Goedel1933fintro,
  editor = 	 {S. Feferman},
  booktitle =    {Kurt Gödel, Collected Works vol.1 (Publications 1929--1936)},
  publisher = 	 {Oxford},
  year = 	 {1986},
  author =	 {A.S. Troelstra},
  title =        {Introductory note to 1933f},
  pages =        {296--299},
}





% «bib-Gratzer»  (to ".bib-Gratzer")
% (find-books "__alg/__alg.el" "gratzer")
% 
@Book{Gratzer,
  author = 	 {G. Grätzer},
  title = 	 {Lattice Theory: Foundation},
  publisher = 	 {Birkhäuser},
  year = 	 {2011},
}







% «bib-HellerTierney»  (to ".bib-HellerTierney")
% (to "bib-Freyd76")
% Freyd's paper that was a predecessor to Cats & Alligators was published
% here... What are its exact name and page range?
%
@Book{HellerTierney,
  editor = 	 {A. Heller and M. Tierney},
  title = 	 {Algebra, Topology and Category Theory: A Collection of Papers in Honour of Samuel Eilenberg},
  publisher = 	 {Academic Press},
  year = 	 {1976},
}


% «bib-HylandPitts»  (to ".bib-HylandPitts")
% J. M. E. Hyland and A. M. Pitts. The theory of constructions:
% Categorical semantics and topos-theoretic models. In Categories in
% Computer Science and Logic, pages 137-- 199. AMS, 1987. AMS
% Contemporory Mathematics Series 92.
%
@InProceedings{HylandPitts,
  author = 	 {J. M. E. Hyland and A. M. Pitts},
  title = 	 {The theory of constructions: Categorical semantics
		  and topos-theoretic models},
  booktitle =	 {Categories in Computer Science and Logic},
  pages =	 {137--199},
  year =	 {1987},
  number =	 {92},
  series =	 {AMS Contemporary Mathematics Series},
  publisher =	 {AMS},
}

% «bib-Jacobs»  (to ".bib-Jacobs")
% (find-books "__cats/__cats.el" "jacobs")
% Bart Jacobs. Categorical Logic and Type Theory. Number 141 in Studies
% in Logic and the Foundations of Mathematics. North Holland, Elsevier,
% 1999.
%
@Book{Jacobs,
  author =	 {B. Jacobs},
  title = 	 {Categorical Logic and Type Theory},
  publisher = 	 {North-Holland, Elsevier},
  year = 	 1999,
  number =	 141,
  series =	 {Studies in Logic and the Foundations of Mathematics},
}

% «bib-Jamnik»  (to ".bib-Jamnik")
% http://www.cl.cam.ac.uk/~mj201/research/book/index.html
%
@Book{Jamnik,
  author = 	 {M. Jamnik},
  title = 	 {Mathematical Reasoning with Diagrams: From Intuition
                  to Automation},
  publisher = 	 {CSLI},
  year = 	 {2001},
}

% «bib-Johnstone»  (to ".bib-Johnstone")
% (find-LATEX "filters.bib" "johnstone")
% (find-angg ".emacs.papers" "johnstone")
%
@Book{Johnstone,
  author =	 {P. T. Johnstone},
  title = 	 {Topos Theory},
  publisher = 	 {Academic Press},
  year = 	 {1977},
}
@Book{Elephant1,
  author =	 {P. T. Johnstone},
  title = 	 {Sketches of an Elephant: A Topos Theory Compendium},
  publisher = 	 {Oxford University Press},
  volume =       {1},
  year = 	 {2002},
}
@Book{Elephant2,
  author =	 {P. T. Johnstone},
  title = 	 {Sketches of an Elephant: A Topos Theory Compendium},
  publisher = 	 {Oxford University Press},
  volume =       {2},
  year = 	 {2002},
}

% «bib-JoyalStreet»  (to ".bib-JoyalStreet")
% http://www.math.mq.edu.au/~street/Publications.html
%
@Article{JoyalStreet,
  author = 	 {A. Joyal and R. Street},
  title = 	 {The geometry of tensor calculus I},
  journal = 	 {Advances in Mathematics},
  year = 	 {1991},
  volume = 	 {88},
  pages = 	 {55--112},
}

% «bib-Kamareddine»  (to ".bib-Kamareddine")
% (find-books "__logic/__logic.el" "typetheory")
%
@Book{Kamareddine,
  author = 	 {F. Kamareddine and T. Laan and R. Nederperlt},
  title = 	 {A Modern Perspective on Type Theory},
  publisher = 	 {Kluwer},
  year = 	 {2004},
}

% «bib-KellyLack»  (to ".bib-KellyLack")
% (find-angg ".emacs.papers" "kelly")
%
@Article{KellyLack,
  author = 	 {J. Kelly, S. Lack},
  title = 	 {On Property-Like Structures},
  journal = 	 {Theory and Applications of Categories},
  year = 	 {1997},
  pages = 	 {??-??},
  note =	 {\url{http://www.tac.mta.ca/tac/volumes/1997/n9/n9.dvi}}
}

% «bib-Kock77»  (to ".bib-Kock77")
% (find-THfile "math-b.blogme" "A simple axiomatics for differentiation")
% (find-THfile "math-b.blogme" "www.mscand.dk")
% (find-angg ".emacs.papers" "kock")
%
@Article{Kock77,
  author = 	 {A. Kock},
  title = 	 {A simple axiomatics for differentiation},
  journal = 	 {Mathematica Scandinavica},
  year = 	 {1977},
  volume = 	 {40},
  number = 	 {2},
  pages = 	 {183-193},
  note =	 {\url{http://www.mscand.dk/article.php?id=2356}},
}

% «bib-Kock81»  (to ".bib-Kock81")
% (find-angg ".emacs.papers" "kock")
% http://home.imf.au.dk/kock/sdg99.pdf
@Book{Kock81,
  author = 	 {A. Kock},
  title = 	 {Synthetic Differential Geometry},
  publisher = 	 {Cambridge},
  year = 	 {1980},
  note =         {\url{http://home.imf.au.dk/kock/sdg99.pdf}},
}

% «bib-Kromer»  (to ".bib-Kromer")
% (find-books "__cats/__cats.el" "kromer")
@Book{Kromer,
  author =	 {R. Krömer},
  title = 	 {Tool and Object: A History and Philosophy of Category Theory},
  publisher = 	 {Birkhäuser},
  year = 	 {2007},
}

% «bib-LambekScott»  (to ".bib-LambekScott")
% (find-books "__cats/__cats.el" "lambek-scott")
%
@Book{LambekScott,
  author = 	 {J. Lambek and P. Scott},
  title = 	 {Introduction to Higher-Order Categorical Logic},
  publisher = 	 {Cambridge},
  year = 	 {1986},
}

% «bib-LangAlgebra»  (to ".bib-LangAlgebra")
@Book{LangAlgebra,
  author = 	 {S. Lang},
  title = 	 {Algebra, 3rd ed.},
  publisher = 	 {Springer},
  year = 	 {2002},
}

% «bib-Lavendhomme»  (to ".bib-Lavendhomme")
@Book{Lavendhomme,
  author = 	 {R. Lavendhomme},
  title = 	 {Basic Concepts of Synthetic Differential Geometry},
  publisher = 	 {Kluwer},
  year = 	 {1996},
}

% «bib-Lawvere80»  (to ".bib-Lawvere80")
%
@Article{Lawvere80,
  author = 	 {W. Lawvere},
  title = 	 {Toward the Description in a Smooth Topos of the
		  Dynamically Possible Motions and Deformations of a
		  Continuous Body},
  journal = 	 {Cahiers de Topologie et Géométrie Différentielle
		  Catégorique},
  year = 	 {1980},
  volume = 	 {XXI},
  pages = 	 {337--392},
}

% «bib-LawvereAdjBicat»  (to ".bib-LawvereAdjBicat")
% W. Lawvere - Adjoints in and among Bicategories, Proceedings of the
% 1994 Siena Conference in Memory of Roberto Magari. Logic & Algebra,
% Lecture Notes in Pure and Applied Algebra 180: 181-189, Ed.
% Ursini/Aglianò, Marcel Dekker, Inc. Basel, New York, 1996.
%
@InProceedings{LawvereAdjBicat,
  author = 	 {W. Lawvere},
  title = 	 {Adjoints in and among Bicategories},
  booktitle =	 {Proceedings of the 1994 Siena Conference in Memory of
		  Roberto Magari},
  pages =	 {181--189},
  year =	 {1996},
  editor =	 {Ursini and Aglianò},
  number =	 {180},
  series =	 {Logic \& Algebra, Lecture Notes in Pure and Applied Algebra},
  publisher =	 {Marcel Dekker, Inc. Basel, New York},
}

% «bib-LawvereAdjFo»  (to ".bib-LawvereAdjFo")
% (find-angg ".emacs.papers" "lawvere")
%
@Article{LawvereAdjFo,
  author = 	 {W. Lawvere},
  title = 	 {Adjointness in Foundations},
  journal = 	 {Dialectica},
  year = 	 {1969},
  volume = 	 {23},
  pages = 	 {281--296},
}

% «bib-LawvereEqHyp»  (to ".bib-LawvereEqHyp")
% (find-books "__cats/__cats.el" "lawvere")
%
@Article{LawvereEqHyp,
  author = 	 {W. Lawvere},
  title = 	 {Equality in Hyperdoctrines and Comprehension Schema as an Adjoint Functor},
  journal = 	 {Proceedings of the American Mathematical Society Symposium on Pure Mathematics XVII},
  year = 	 {1970},
  volume = 	 {999},
  pages = 	 {1--14},
}

% «bib-LawvereSchanuel»  (to ".bib-LawvereSchanuel")
% (find-books "__cats/__cats.el" "lawvere")
%
@Book{LawvereSchanuel,
  author = 	 {W. Lawvere and S. Schanuel},
  title = 	 {Conceptual Mathematics: A first introduction to categories},
  publisher = 	 {Cambridge},
  year = 	 {1997},
}

% «bib-LawvereThesis»  (to ".bib-LawvereThesis")
% (find-angg ".emacs.papers" "lawvere")
%
@PhdThesis{LawvereThesis,
  author = 	 {W. Lawvere},
  title = 	 {Functorial Semantics of Algebraic Theories},
  school = 	 {Berkeley?},
  year = 	 {1963},
  note = 	 {\url{http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html}},
}


% «bib-Luo»  (to ".bib-Luo")
% (find-angg ".emacs.papers" "luo")
%
@PhdThesis{Luo,
  author = 	 {Z. Luo},
  title = 	 {An Extended Calculus of Constructions},
  school = 	 {University of Edinburgh},
  year = 	 {1990},
  note =	 {Also as Report CST-65-90/ECS-LFCS-90-118,
                  Department of Computer Science, University of Edinburgh},
}

% «bib-Macbeth»  (to ".bib-Macbeth")
% (find-books "__frege/__frege.el" "macbeth")
%
@Book{Macbeth,
  author = 	 {D. Macbeth},
  title = 	 {Frege's Logic},
  publisher = 	 {Harvard},
  year = 	 {2005},
}


% «bib-MacLane»  (to ".bib-MacLane")
% (find-books "__cats/__cats.el" "maclane")
%
@Book{CWM,
  author = 	 {S. MacLane},
  title = 	 {Categories for the Working Mathematician},
  publisher = 	 {Springer},
  year = 	 {1971},
}

% «bib-MacLaneMoerdijk»  (to ".bib-MacLaneMoerdijk")
% S.MacLane and I.Moerdijk, Sheaves in geometry and logic: a first
% introduction to topos theory, Springer-Verlag, 1992.
%
@Book{MacLaneMoerdijk,
  author =	 {S. MacLane and I. Moerdijk},
  title = 	 {Sheaves in geometry and logic: a first introduction
		  to topos theory},
  publisher = 	 {Springer},
  year = 	 {1992},
}

% «bib-MartinLof84»  (to ".bib-MartinLof84")
@Book{MartinLof84,
  author = 	 {P. Martin-Löf},
  title = 	 {Intuitionistic Type Theory},
  publisher = 	 {Bibliopolis},
  year = 	 {1984},
  series = 	 {Studies in Proof Theory},
  address = 	 {Napoli}
}

% «bib-McLarty»  (to ".bib-McLarty")
% (find-books "__cats/__cats.el" "mclarty")
% Colin McLarty. Elementary Categories, Elementary Toposes. Number 21
% in Oxford Logic Guides. Oxford University Press, 1992.
%
% p.168: "The idea of a later stage of definition appears in Kripke's
% semantics (although not the term `stage of definition', which seems
% to be derived from algebraic geometry, where a given polynomial has
% solutions `defined over' various fields)."
%
@Book{McLarty,
  author =	 {C. McLarty},
  title = 	 {Elementary Categories, Elementary Toposes},
  publisher = 	 {Oxford University Press},
  year = 	 {1992},
  number =	 {21},
  series =	 {Oxford Logic Guides},
}


% «bib-ModalHandbook» (to ".bib-ModalHandbook")
% (find-books "__modal/__modal.el" "handbook")
% (find-handbookmodalpage (+ 39 427) "Wolter")
% (find-handbookmodalpage (+ 39 449) "Transitive logics of finite depth and width")
%
@InBook{ModalHandbook,
  editor =	 {P. Blackburn and J. van Benthem and F. Wolter},
  author =	 {F. Wolter and M. Zakharyaschev},
  title = 	 {Handbook of Modal Logic},
  chapter = 	 {Modal Decision Problems},
  publisher = 	 {Elsevier},
  year = 	 {2007},
  pages =	 {427--489},
}


% «bib-MoeRey»  (to ".bib-MoeRey")
% (find-books "__cats/__cats.el" "moerdijk")
%
@Book{MoeRey,
  author =	 {I. Moerdijk and G. E. Reyes},
  title = 	 {Models for Smooth Infinitesimal Analysis},
  publisher = 	 {Springer},
  year = 	 {1991},
}

% «bib-Ochs»  (to ".bib-Ochs")
% (find-TH "math-b" "MsC")
% (find-TH "math-b" "2000-UFF")
% (find-TH "math-b" "filter-infinitesimals")
% (find-TH "math-b" "internal-diags-in-ct")
% (find-TH "math-b" "zhas-for-children-2")
% https://link.springer.com/journal/11787/7/3/page/1 LU containing idarct
% https://link.springer.com/article/10.1007/s11787-013-0083-z idarct
%
@MastersThesis{OchsMsC,
  author = 	 {E. Ochs},
  title = 	 {Categorias, Filtros e Infinitesimais Naturais},
  school = 	 {PUC-Rio},
  year = 	 {1999},
  note = 	 {\url{http://angg.twu.net/math-b.html#MsC}},
}
@Unpublished{OchsFilters08,
  author = 	 {E. Ochs},
  title = 	 {Natural Infinitesimals in Filter-Powers},
  note = 	 {Notes, \url{http://angg.twu.net/math-b.html#filter-infinitesimals}},
  year = 	 {2008},
}
@Unpublished{OchsUniLog,
  author = 	 {E. Ochs},
  title = 	 {Downcasing Types},
  note = 	 {Slides for a presentation at the UniLog'2010. \url{http://angg.twu.net/math-b.html#unilog-2010}},
  year = 	 {2010},
}
@Unpublished{OchsIDCT,
  author = 	 {E. Ochs},
  title = 	 {Internal Diagrams in Category Theory},
  note = 	 {Submitted (to {\sl Logica Universalis})},
  year = 	 {2010},
}
@Unpublished{OchsDownHyp,
  author = 	 {E. Ochs},
  title = 	 {Downcasing Hyperdoctrines},
  note = 	 {In preparation},
  year = 	 {2011},
}
@Article{OchsIDARCT,
  author = 	 {E. Ochs},
  title =        {Internal Diagrams and Archetypal Reasoning in Category Theory},
  journal = 	 {Logica Universalis},
  year = 	 {2013},
  month =	 {september},
  volume =	 {7},
  number =	 {3},
  pages =	 {291--321},
}




% «bib-Pavlovic»  (to ".bib-Pavlovic")
%
@PhdThesis{Pavlovic,
  author = 	 {D. Pavlovi\'c},
  title = 	 {Predicates and Fibrations},
  school = 	 {University of Utrecht},
  year = 	 {1990},
}

% «bib-Phoa»  (to ".bib-Phoa")
% Wesley Phoa. An introduction to fibrations, topos theory, the
% effective topos, and modest sets. Technical Report ECS-LFCS-92-208,
% LFCS Edinburgh, 1992.
%
@TechReport{Phoa,
  author = 	 {W. Phoa},
  title = 	 {An introduction to fibrations, topos theory, the
		  effective topos, and modest sets},
  institution =  {LFCS Edinburgh},
  year = 	 {1992},
  note =	 {Technical Report ECS-LFCS-92-208},
}

% «bib-Pitts»  (to ".bib-Pitts")
% (find-angg ".emacs.papers" "pitts")
% http://www.cl.cam.ac.uk/~amp12/bib/PittsAM.bib
%
@INPROCEEDINGS{PittsAM:polist,
  AUTHOR =	 {A.~M.~Pitts},
  TITLE =	 {Polymorphism Is Set Theoretic, Constructively},
  BOOKTITLE =	 {Category Theory and Computer Science, Proc.\
                  Edinburgh 1987},
  EDITOR =	 {D.~H.~Pitt and A.~Poign{\'e} and D.~E.~Rydeheard},
  SERIES =	 {Lecture Notes in Computer Science},
  PUBLISHER =	 {Springer-Verlag, Berlin},
  VOLUME =	 283,
  YEAR =	 1987,
  PAGES =	 {12--39}
}

% «bib-Prawitz65»  (to ".bib-Prawitz65")
%
@Book{Prawitz65,
  author =	 {D. Prawitz},
  title = 	 {Natural Deduction},
  publisher = 	 {Almqvist \& Wiksell, Stockholm, Sweden},
  year = 	 {1965},
}

% «bib-PrawitzIRPF»  (to ".bib-PrawitzIRPF")
%
@InProceedings{PrawitzIRPF,
  author = 	 {D. Prawitz},
  title = 	 {Ideas and results in proof theory},
  booktitle =	 {Proceedings of the Second Scandinavian Logic Symposium},
  pages =	 {235--307},
  year =	 {1971},
  editor =	 {J.E. Fenstad},
  publisher =	 {North-Holland},
}

% «bib-Reyes»  (to ".bib-Reyes")
% (find-books "__cats/__cats.el" "reyes")
%
@Book{ReyesZolf,
  author =	 {M. P. Reyes and G. E. Reyes and H. Zolfaghari},
  title = 	 {Generic Figures and Their Glueings},
  publisher = 	 {Polimetrica},
  year = 	 {2004},
}


% «bib-Schalk»  (to ".bib-Schalk")
% (find-angg ".emacs.papers" "schalk")
@Unpublished{Schalk,
  author = 	 {A. Schalk},
  title = 	 {Some Notes on Monads},
  note = 	 {\url{http://www.cs.man.ac.uk/~schalk/notes/monads.ps.gz}},
  year =	 {2002},
}

% «bib-SeelyBeck»  (to ".bib-SeelyBeck")
% (find-angg ".emacs.papers" "seely")
% (find-ragshyppage (+ -504 513))
%
@article{SeelyBeck,
 author		= {R. A. G. Seely},
 title		= {Hyperdoctrines, natural deduction, and the Beck condition},
 journal	= {Zeitschrift f. math. Logik und Grundlagen d. Math.},
 volume		= {29},
 pages		= {505--542},
 year		= {1983}
}

% «bib-SeelyCartDiff»  (to ".bib-SeelyCartDiff")
% (find-angg ".emacs.papers" "seely")
% (find-ragscartdiffpage 1)
% (find-ragscartdifftext)
%
@Unpublished{SeelyCartDiff,
  author = 	 {R. F. Blute and J. R. B. Cockett and R. A. G. Seely},
  title = 	 {Cartesian Differential Categories},
  note = 	 {\url{http://www.math.mcgill.ca/rags/difftl/cartdiff.pdf}},
  year = 	 {2008},
}

% «bib-SeelyDiff»  (to ".bib-SeelyDiff")
% (find-angg ".emacs.papers" "seely-diff")
% (find-ragsdiffpage 1)
% (find-ragsdifftext)
%
@Article{SeelyDiff,
  author = 	 {R. Blute and R. Cockett and R. A. G. Seely},
  title = 	 {Differential Categories},
  journal = 	 {Mathematical Structures in Computer Science},
  volume =	 {16},
  pages =	 {1049--1083},
  year = 	 {2006},
}

% «bib-SeelyLCCC»  (to ".bib-SeelyLCCC")
% (find-angg ".emacs.papers" "seely-lccc")
% (find-ragslcccpage (+ -32 33))
%
@Article{SeelyLCCC,
  author = 	 {R. A. G. Seely},
  title = 	 {Locally Cartesian closed categories and type theory},
  journal = 	 {Math. Proc. Cambridge Philos. Soc.},
  year = 	 {1984},
  volume =	 {95},
  number =	 {1},
  pages =	 {33--48},
}


% «bib-SeelyPLC»  (to ".bib-SeelyPLC")
% (find-angg ".emacs.papers" "seely-plc")
%               ftp://ftp.math.mcgill.ca/pub/rags/SeelyRAG.bib
% (find-fline "$S/ftp/ftp.math.mcgill.ca/pub/rags/SeelyRAG.bib" ":cshoplc")
% (find-fline "$S/ftp/ftp.math.mcgill.ca/pub/rags/SeelyRAG.bib" ":lccctt")
% month		= {dec},
%
@article{SeelyPLC,
 author		= {R. A. G. Seely},
 title		= {Categorical Semantics for Higher Order Polymorphic
                   Lambda Calculus},
 journal	= {Journal of Symbolic Logic},
 volume		= {52},
 number		= {4},
 pages		= {969--988},
 year		= {1987}
}

% «bib-SmithGalois»  (to ".bib-SmithGalois")
% (find-angg ".emacs.papers" "lawvere-smith")
%
@Unpublished{SmithGalois,
  author = 	 {P. Smith},
  title = 	 {Notes on Galois Connections},
  note = 	 {\url{http://logicmatters.blogspot.com/2008/05/galois-connections.html}},
}


% «bib-Simmons»  (to ".bib-Simmons")
% (find-angg ".emacs.papers" "simmons")
%
@Unpublished{Simmons,
  author = 	 {H. Simmons},
  title = 	 {The point-free approach to sheafification},
  note = 	 {\url{http://www.cs.man.ac.uk/~hsimmons/DOCUMENTS/papersandnotes.html}},
  year = 	 {2001},
}


% «bib-Streicher»  (to ".bib-Streicher")
% (find-angg ".emacs.papers" "streicher")
%
@Unpublished{StreicherBenabou,
  author = 	 {T. Streicher},
  title = 	 {Fibred Categories à là {J}. {B}énabou},
  note = 	 {Notes},
  month = 	 {April},
  year = 	 {1999},
}

% «bib-Taylor»  (to ".bib-Taylor")
% (find-angg ".emacs.papers" "taylor")
% 
@PhdThesis{TaylorPhDThesis,
  author = 	 {P. Taylor},
  title = 	 {Recursive Domains, Indexed Category Theory and Polymorphism},
  school = 	 {Cambridge},
  year = 	 {1986},
}

% «bib-WadlerGR»  (to ".bib-WadlerGR")
% Philip Wadler. The Girard-Reynolds isomorphism. In N. Kobayashi and B.
% C. Pierce, editors, Proc. of 4th Int. Symp. on Theoretical Aspects of
% Computer Science, TACS 2001.
%
@InProceedings{WadlerGR,
  author = 	 {P. Wadler},
  title = 	 {The {G}irard-{R}eynolds isomorphism},
  booktitle =	 {Proc. of 4th Int. Symp. on Theoretical Aspects of
		  Computer Science, TACS 2001},
  year =	 {2001},
  editor =	 {N. Kobayashi and B. C. Pierce},
}

% «bib-WadlerTfF»  (to ".bib-WadlerTfF")
% Wadler, P.: Theorems for Free!, Proc. FPCA'89 , ACM, pp.347--359
% (1989).
%
@InProceedings{WadlerTfF,
  author = 	 {P. Wadler},
  title = 	 {Theorems for Free!},
  booktitle =	 {Proc. FPCA'89},
  pages =	 {347--359},
  year =	 {1989},
  publisher =	 {ACM},
}



% «bib-LuaGems»  (to ".bib-LuaGems")
% (to "bib-Bootstrapping")
@Book{LuaGems,
  editor = 	 "L. H. de Figueiredo and W. Celes and R. Ierusalimschy",
  booktitle = 	 "Lua Programming Gems",
  publisher = 	 "Lua.org",
  year = 	 "2008",
}




% «bib-Reynolds»  (to ".bib-Reynolds")
% (find-angg ".emacs.papers" "reynolds")
%
@Article{ReynoldsPinST,
  author = 	 {J. Reynolds},
  title = 	 {Polymorphism is not Set-Theoretic},
  journal = 	 {LNCS ???},
  year = 	 {1984},
  note = 	 {preprint version: \url{http://www.inria.fr/rrrt/rr-0296.html}},
}

% Pitts: Polymorphism is Set-Theoretic, constructively
%   Seely: Categorical Semantics for Higher Order Polymorphic Lambda Calculus
% 
% Lawvere (easy book): external/internal view
% Lawvere: hyperdoctrines ("healthy start")
% 
% Freyd: Algebraic categories



% (describe-bindings "\C-c\C-e")

% Main missing entries:
%   Hindley/Seldin
%   Streicher (Benabou)
%   Izumi Takeuti
%   Kock - book, article about e^2=0, kock/mitchell
%   Lavendhomme

% (find-books "__logic/__logic.el" "hindley")
% (find-angg ".emacs.papers" "streicher")

% Proofs are Programs: 19th Century Logic and 21st Century Computing
% 
% Philip Wadler. (This is a variant of New Languages, Old Logic, which
% appeared in Dr Dobbs Journal, special supplement on Software in the
% 21st century, December 2000. There is also an Netcast interview.)
% 
%        + Phil Wadler:
%             o Theorems for Free! (1989), The Girard-Reynolds
%               Isomorphism (2001) (rmt)
%             o Proofs are Programs: 19th Century Logic and 21st Century
%               Computing (rmt)
%        + John Reynolds:
%             o On Functors Expressible in the Polymorphic Typed Lambda
%               Calculus (rmt)
%        + Izumi Takeuti:
%             o An Axiomatic System of Parametricity (rmt) (1998)
%             o The Theory of Parametricity in Lambda Cube (rmt) (draft)
%        + Harry Mairson:
%             o Outline of a Proof Theory of Parametricity (rmt)
%   * On Non-standard Analysis, SDG and friends:
%        + A page with many links on Non-Standard Analysis (rmt)
%        + William Lawvere (rmt):
%             o Outline of Synthetic Differential Geometry (rmt) (1998)
%             o Toposes of Laws of Motion (rmt) (1997)
% 
%        + Thomas Ehrhard (rmt): The Differential Lambda-Calculus (rmt)
%          (2001).
%        + Anders Kock (rmt):
%             o Aspects of Fractional Exponent Functors (rmt) (1999,
%               with G. Reyes)
%             o Fractional Exponent Functors and Categories of
%               Differential Equations (rmt) (1998, with G. Reyes)

% Phil Scott
% Andy Pitts

% Robinson: NSA

% Add:
% Freyd's short thing

% (find-angg ".emacs.papers" "beck")
% (find-angg ".emacs.papers" "kelly")
% (find-angg ".emacs.papers" "taylor")

% «diagrams»  (to ".diagrams")
% (find-LATEX "catsem.bib" "bib-Jamnik")
% (find-angg ".emacs.papers" "cheng")
% (find-books "__cats/__cats.el" "freyd-scedrov")
% (find-books "__cats/__cats.el" "kromer")
% (find-books "__cats/__cats.el" "reyes")
% (find-books "__frege/__frege.el" "macbeth")
% (find-books "__phil/__phil.el" "corfield")



% Local variables:
% coding: raw-text-unix
% modes: (bibtex-mode fundamental-mode)
% end: