Warning: this is an htmlized version!
The original is here, and
the conversion rules are here.
% This file:
%   http://angg.twu.net/LATEX/catsem-slides.bib.html
%   http://angg.twu.net/LATEX/catsem-slides.bib
%           (find-angg "LATEX/catsem-slides.bib")
% Author: Eduardo Ochs <eduardoochs@gmail.com>
%
% This is a version of 
%
%           (find-angg "LATEX/catsem-u.bib")
%
% that is written in UTF-8, intended to be used by biber, and in which
% most entries have shorthands - like [IDARCT] - and hyperliks.
%
% (defun b  () (interactive) (find-angg "LATEX/catsem-slides.bib"))
% (defun b0 () (interactive) (find-angg "LATEX/catsem-u.bib"))


% «.bib-WadlerSMBF»	(to "bib-WadlerSMBF")
% «.bib-DSLS»		(to "bib-DSLS")
% «.bib-Ganesalingam»	(to "bib-Ganesalingam")
% «.bib-HuCarette»	(to "bib-HuCarette")


% (find-books "__comp/__comp.el" "abelson-sussman")
%
@Book{SICP,
  author = 	 {H. Abelson and G.J. Sussman},
  title = 	 {Structure and Interpretation of Computer Programs, 2nd ed},
  publisher = 	 {MIT},
  year = 	 {1996},
  note =         {\url{https://web.mit.edu/alexmv/6.037/sicp.pdf}},
  shorthand =    {SICP},
}

% (find-books "__cats/__cats.el" "awodey")
%
@Book{Awodey,
  author =	 {S. Awodey},
  title = 	 {Category Theory},
  publisher = 	 {Oxford},
  year = 	 {2006},
}

% (find-books "__cats/__cats.el" "badiou-low")
%
@Book{BadiouLoW,
  author = 	 {A. Badiou},
  title = 	 {Logics of Worlds - Being and Event, 2},
  publisher = 	 {Continuum},
  year = 	 {2009},
}

% (find-books "__cats/__cats.el" "badiou-mt")
%
@Book{BadiouMoTT,
  author = 	 {A. Badiou},
  title = 	 {Mathematics of The Transcendental},
  publisher = 	 {Bloomsbury},
  year = 	 {2014},
}

% (find-books "__cats/__cats.el" "bell")
% 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},
}

% (find-books "__cats/__cats.el" "caccamo-phd")
%
@PhdThesis{CaccamoPhD,
  author = 	 {M. J. Cáccamo},
  title = 	 {A Formal Calculus for Categories},
  school = 	 {Aarhus},
  year = 	 {2004},
  note = 	 {\url{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.7460}},
}

% (find-books "__cats/__cats.el" "caccamo-winskel")
%
@Unpublished{CaccamoWinskel,
  author = 	 {M. J. Cáccamo and G. Winskel},
  title = 	 {A Higher-Order Calculus for Categories},
  note = 	 {\url{https://www.brics.dk/RS/01/27/BRICS-RS-01-27.pdf}},
  year = 	 {2001},
}

% (find-books "__cats/__cats.el" "cheng-morally")
%
@Unpublished{ChengMorally,
  author = 	 {E. Cheng},
  title = 	 {Mathematics, Morally},
  note = 	 {\url{http://eugeniacheng.com/wp-content/uploads/2017/02/cheng-morality.pdf}},
  year = 	 {2004},
}


% (find-books "__cats/__cats.el" "coecke-newstrup")
%
@Book{CoeckeNewStruP,
  editor = 	 {B. Coecke},
  title = 	 {New Structures for Physics},
  publisher = 	 {Springer},
  year = 	 {2011},
  note =         {\url{https://www.springer.com/br/book/9783642128202}},
}

% (find-books "__cats/__cats.el" "coecke")
%
@Book{CoeckePQP,
  author = 	 {B. Coecke and A. Kissinger},
  title = 	 {Picturing Quantum Processes. A First Course in
                  Quantum Theory and Diagrammatic Reasoning},
  publisher = 	 {Cambridge},
  note =         {\url{http://www.cambridge.org/gb/pqp}},
  year = 	 {2017},
}

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

% (find-LATEX "catsem-u.bib" "bib-Eilenberg")
%
@Book{EilenbergSteenrod,
  author = 	 {S. Eilenberg and N. Steenrod},
  title = 	 {Foundations of algebraic topology},
  publisher = 	 {Princeton},
  year = 	 {1952},
  shorthand =    {ES52},
}

% (find-TH "emacsconf2019")
%
@Misc{Eev2019,
  author = 	 {E. Ochs},
  title = 	 {How to record executable notes with eev - and how to
                  play them back},
  year = 	 {2019},
  note = 	 {\url{http://angg.twu.net/emacsconf2019.html}},
}

@Misc{Emacs81,
  author = 	 {R. Stallman},
  title = 	 {EMACS: The Extensible, Customizable Display Editor},
  year = 	 {1981},
  note = 	 {\url{http://www.gnu.org/software/emacs/emacs-paper.html}},
}

% (find-books "__comp/__comp.el" "free-as-in-freedom")
%
@Book{FaiF,
  author = 	 {S. Williams},
  title = 	 {Free as in Freedom (2.0): Richard Stallman and the
                  Free Software Revolution},
  publisher = 	 {FSF},
  year = 	 {2010},
  note = 	 {\url{https://static.fsf.org/nosvn/faif-2.0.pdf}},
}

% (find-books "__cats/__cats.el" "fong-spivak")
%
@Book{FongSpivak,
  author = 	 {B. Fong and D. I. Spivak},
  title = 	 {Seven Sketches in Compositionality: An Invitation to
                  Applied Category Theory},
  publisher = 	 {Cambridge},
  year = 	 {2019},
  %note = 	 {\url{http://math.mit.edu/\~dspivak/teaching/sp18/7Sketches.pdf}},
  note = 	 {\url{https://arxiv.org/pdf/1803.05316.pdf}},
}


% (find-LATEX "catsem.bib" "bib-Fourman")
%
@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},
}


% (find-books "__cats/__cats.el" "freyd-aspects")
% [FK] P. Freyd, Aspects of Topoi. Bull. Austral. Math. Soc. 7 (1972), 1-76 and 467-480. MR 53/576.
%
@Article{FreydAspects,
  author = 	 {P. Freyd},
  title = 	 {Aspects of Topoi},
  journal = 	 {Bull. Austral. Math. Soc.},
  year = 	 {1972},
  volume = 	 {7},
  number = 	 {1},
  pages = 	 {1-76},
  note = 	 {\url{https://ncatlab.org/spahn/files/aspects_of_topoi.pdf}},
}

% (find-LATEX "catsem-u.bib" "bib-Freyd76")
%
@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},
  note =         {\url{http://angg.twu.net/Freyd76.html}},
  shorthand =    {Freyd76},
}

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

% (find-books "__logic/__logic.el" "girard")
%
@Book{GLT,
  author = 	 {J.-Y. Girard and Y. Lafont and P. Taylor},
  title = 	 {Proofs and Types},
  publisher = 	 {Cambridge},
  year = 	 {1989},
  note =         {\url{http://www.paultaylor.eu/stable/prot.pdf}},
}

% (find-books "__logic/__logic.el" "girard-blind-spot")
%
@Book{GirardBlind,
  author = 	 {J.-Y. Girard},
  title = 	 {The Blind Spot},
  publisher = 	 {European Mathematical Society},
  year = 	 {2010},
}

% (find-books "__cats/__cats.el" "jacobs")
%
@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},
}


% (find-books "__logic/__logic.el" "jamnik")
% https://www.cl.cam.ac.uk/~mj201/book.html
%
@Book{Jamnik,
  author = 	 {M. Jamnik},
  title = 	 {Mathematical Reasoning with Diagrams: From Intuition
                  to Automation},
  publisher = 	 {CSLI},
  year = 	 {2001},
}


% (find-books "__cats/__cats.el" "johnstone-elephant")
%
@Book{Elephant1,
  author =	 {P. T. Johnstone},
  title = 	 {Sketches of an Elephant: A Topos Theory Compendium},
  publisher = 	 {Oxford},
  volume =       {1},
  year = 	 {2002},
  shorthand =    {Elephant},
}

@Book{Johnstone,
  author =	 {P. T. Johnstone},
  title = 	 {Topos Theory},
  publisher = 	 {Academic Press},
  year = 	 {1977},
}

% (find-books "__cats/__cats.el" "leinster-basic")
%
@Book{Leinster,
  author = 	 {T. Leinster},
  title = 	 {Basic Category Theory},
  publisher = 	 {Cambridge},
  year = 	 {2014},
  shorthand =    {Leinster},
  note =         {\url{https://arxiv.org/pdf/1612.09375.pdf}},
}



% (find-books "__logic/__logic.el" "hott")
%
@Book{HOTT,
  author =       {The {Univalent Foundations Program}},
  title =        {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher =    {Institute for Advanced Study},
  % publisher =  {\url{https://homotopytypetheory.org/book}},
  % address =    {Institute for Advanced Study},
  year =         {2013},
  note =         {\url{http://saunders.phil.cmu.edu/book/hott-online.pdf}},
  shorthand =    {HOTT},
}

% «bib-MacLane»  (to ".bib-MacLane")
% (find-books "__cats/__cats.el" "maclane")
%
@Book{CWM2,
  author = 	 {S. Mac Lane},
  title = 	 {Categories for the Working Mathematician (2nd ed.)},
  publisher = 	 {Springer},
  year = 	 {1997},
  shorthand =    {CWM},
}

% (find-books "__cats/__cats.el" "maclane-bowdoin")
%
@Unpublished{MacLaneNotes,
  author = 	 {S. Mac Lane},
  title = 	 {Lectures on Category Theory (Bowdoin Summer School)},
  year = 	 {1969},
  note = 	 {Handwritten notes by E. Cooper:
                  \url{https://ncatlab.org/nlab/show/Lectures+on+category+theory}},
  shorthand =    {MacLaneNotes},
}

% (find-books "__cats/__cats.el" "maclane-moerdijk")
%
@Book{MacLaneMoerdijk,
  author =	 {S. Mac Lane and I. Moerdijk},
  title = 	 {Sheaves in geometry and logic: a first introduction
		  to topos theory},
  publisher = 	 {Springer},
  year = 	 {1992},
}

@Unpublished{MarsdenCTUSD,
  author = 	 {D. Marsden},
  title = 	 {Category Theory Using String Diagrams},
  note = 	 {\url{https://arxiv.org/pdf/1401.7220.pdf}},
  year = 	 {2014},
}

% (find-LATEX "catsem-u.bib" "bib-McLarty")
% (find-books "__cats/__cats.el" "mclarty")
@Book{McLarty,
  author =	 {C. McLarty},
  title = 	 {Elementary Categories, Elementary Toposes},
  publisher = 	 {Oxford University Press},
  year = 	 {1992},
  number =	 {21},
  series =	 {Oxford Logic Guides},
}

% (find-books "__cats/__cats.el" "milewski-ctfp")
%
@Unpublished{MilewskiCTFPOCaml,
  author = 	 {B. Milewski},
  title = 	 {Category Theory for Programmers, OCaml Edition},
  note = 	 {\url{https://github.com/hmemcpy/milewski-ctfp-pdf/releases/download/v1.4.0-rc1/category-theory-for-programmers-ocaml.pdf}},
  year = 	 {2020},
}

% (find-books "__logic/__logic.el" "negri-vonplato")
%
@Book{NegriVonPlato,
  author = 	 {S. Negri and J. von Plato},
  title = 	 {Structural Proof Theory},
  publisher = 	 {Cambridge},
  year = 	 {2001},
}

@Article{PH1,
  author = 	 {E. Ochs},
  title = 	 {Planar Heyting Algebras for Children},
  journal = 	 {South American Journal of Logic},
  year = 	 {2019},
  volume = 	 {5},
  number = 	 {1},
  pages = 	 {125--164},
  note = 	 {\url{http://angg.twu.net/math-b.html\#zhas-for-children-2}},
  shorthand =    {PH1},
}

@Unpublished{PH2,
  author = 	 {E. Ochs},
  title = 	 {Planar Heyting Algebras for Children 2: Local
                  J-Operators, Slashings, and Nuclei},
  note = 	 {\url{http://angg.twu.net/math-b.html\#zhas-for-children-2}},
  shorthand =    {PH2},
  year = 	 {2021},
}

@Article{IDARCT,
  author = 	 {E. Ochs},
  title =        {Internal Diagrams and Archetypal Reasoning in Category Theory},
  journal = 	 {Logica Universalis},
  year = 	 {2013},
  month =	 {9},
  volume =	 {7},
  number =	 {3},
  pages =	 {291--321},
  note = 	 {\url{http://angg.twu.net/math-b.html\#idarct}},
  shorthand =    {IDARCT},
}

% (lfc)
@Unpublished{OchsLucatelli,
  author = 	 {E. Ochs and F. Lucatelli},
  title = 	 {Logic for Children - Workshop at UniLog 2018 (Vichy) -
                  unofficial homepage},
  note =         {\url{http://angg.twu.net/logic-for-children-2018.html}},
  year = 	 {2018},
}

% (find-TH "math-b" "visualizing-gms-unilog-2018")
%
@Unpublished{OchsVGMS2018,
  author = 	 {E. Ochs},
  title = 	 {Visualizing Geometric Morphisms},
  note = 	 {\url{http://angg.twu.net/LATEX/2018vichy-vgms-slides.pdf}},
  year = 	 {2018},
}


% (find-math-b-links "wld-2019" "2019logicday")
%
@Unpublished{OchsWLD2019,
  author = 	 {E. Ochs},
  title = 	 {How to almost teach Intuitionistic Logic to Discrete Mathematics Students},
  note = 	 {\url{http://angg.twu.net/LATEX/2019logicday.pdf}},
  year = 	 {2019},
}

@Unpublished{LessMS,
  author = 	 {E. Ochs},
  title = 	 {On two tricks to make Category Theory fit in less
                  mental space: missing diagrams and skeletons of
                  proofs},
  note = 	 {\url{http://angg.twu.net/LATEX/2019newton-slides.pdf}},
  year = 	 {2019},
  shorthand =    {LessMS},
}



% (find-math-b-links "missing-diagrams-elephant" "2019oxford-abs")
%
@Unpublished{MDE,
  author = 	 {E. Ochs},
  title = 	 {On Some Missing Diagrams in The Elephant},
  note = 	 {\url{http://angg.twu.net/math-b.html\#missing-diagrams-elephant}},
  year = 	 {2019},
  shorthand = 	 {MDE},
}

% (find-math-b-links "2020-tallinn" "2020tallinn-abstract")
%
@Unpublished{OchsTallinnAbs,
  author = 	 {E. Ochs},
  title =        {What kinds of knowledge do we gain by doing Category
                  Theory in several levels of abstraction in
                  parallel?},
  note =         {\url{http://angg.twu.net/math-b.html\#2020-tallinn}},
  year =         {2020},
}

% (find-math-b-links "favorite-conventions" "2020favorite-conventions")
%
@Unpublished{FavC,
  author = 	 {E. Ochs},
  title = 	 {On my favorite conventions for drawing the missing
                  diagrams in Category Theory},
  note = 	 {\url{http://angg.twu.net/math-b.html\#favorite-conventions}},
  year = 	 {2020},
  shorthand = 	 {FavC},
}

% (find-math-b-links "clops-and-tops" "2020clops-and-tops")
%
@Unpublished{ClopsAndTops,
  author = 	 {E. Ochs},
  title = 	 {Each closure operator induces a topology and vice-versa},
  note = 	 {\url{http://angg.twu.net/math-b.html\#clops-and-tops}},
  year = 	 {2020},
}

% (find-books "__cats/__cats.el" "perrone")
%
@Unpublished{Perrone,
  author = 	 {P. Perrone},
  title = 	 {Notes on Category Theory with examples from basic mathematics},
  note = 	 {\url{https://arxiv.org/abs/1912.10642}},
  year = 	 {2020},
  shorthand =    {Perrone},
}


% (find-books "__cats/__cats.el" "power")
%
@Article{PowerPasting,
  author = 	 {A. J. Power},
  title = 	 {A 2-Categorical Pasting Theorem},
  journal = 	 {Journal of Algebra},
  year = 	 {1990},
  volume = 	 {129},
  number = 	 {2},
  pages = 	 {439-445},
  note = 	 {\url{https://core.ac.uk/download/pdf/81929927.pdf}},
}


@Book{Prawitz65,
  author =	 {D. Prawitz},
  title = 	 {Natural Deduction},
  publisher = 	 {Almqvist \& Wiksell, Stockholm, Sweden},
  year = 	 {1965},
}


@Book{Riehl,
  author = 	 {E. Riehl},
  title = 	 {Category Theory in Context},
  publisher = 	 {Dover},
  year = 	 {2016},
  note =         {\url{http://www.math.jhu.edu/~eriehl/context.pdf}},
  shorthand =    {Riehl},
}

% (find-books "__cats/__cats.el" "seely-hyp")
%
@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},
 note           = {\url{http://www.math.mcgill.ca/rags/ZML/ZML.PDF}},
}

% (find-books "__cats/__cats.el" "seely-lccc")
%
@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},
  note =         {\url{http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf}},
}

% (find-books "__cats/__cats.el" "seely-plc")
%
@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},
  note =         {\url{http://www.math.mcgill.ca/rags/JSL/PLC.pdf}},
}

% (find-books "__cats/__cats.el" "seely-diff")
%
@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},
  note =         {\url{http://www.math.mcgill.ca/rags/difftl/difftl.pdf}},
}


@Article{WadlerPaT,
  author = 	 {P. Wadler},
  title = 	 {Propositions as Types},
  journal = 	 {Communications of the ACM},
  year = 	 {2015},
  volume = 	 {58},
  number = 	 {12},
  pages = 	 {75--84},
  month = 	 {December},
  note =       {\url{http://homepages.inf.ed.ac.uk/wadler/topics/history.html\#propositions-as-types}},
  shorthand =    {WadlerPaT},
}

% (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},
  note =         {\url{https://www.springer.com/gp/book/9783764375232}},  
}

% (find-books "__cats/__cats.el" "kromer-slides")
%
@Unpublished{KromerSlides,
  author = 	 {R. Krömer},
  title = 	 {Category theory and its foundations: the role of
                  diagrams and other ``intuitive'' material},
  note = 	 {Slides for his keynote talk at the UniLog 2018.
                  \url{http://angg.twu.net/logic-for-children-2018/ralf_kroemer__slides.pdf}},
  year = 	 {2018},
}

% (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}
}




% (find-books "__comp/__comp.el" "penrose")
%
@InProceedings{PenroseSIGGRAPH2020,
  author = 	 {K. Ye et al},
  title = 	 {Penrose: From Mathematical Notation to Beautiful Diagrams},
  year = 	 {2020},
  note = 	 {\url{http://penrose.ink/media/Penrose_SIGGRAPH2020.pdf}},
  shorthand =    {Penrose},
}

@misc{IdrisCT2019,
  title =        {idris-ct: A Library to do Category Theory in Idris},
  author =       {F. Genovese and A. Gryzlov and J. Herold and A.
                  Knispel and M. Perone and E. Post and A. Videla},
  year =         {2019},
  eprint =       {1912.06191},
  archivePrefix = {arXiv},
  primaryClass = {cs.LO},
  shorthand =    {IdrisCT},
}



% (find-books "__comp/__comp.el" "brady")
%
@Book{Brady,
  author = 	 {E. Brady},
  title = 	 {Type-Driven Development With Idris},
  publisher = 	 {Manning},
  year = 	 {2017},
}

% (find-books "__cats/__cats.el" "abramsky-tzevelekos")
%
@Unpublished{AbramskyTzevelekos,
  author = 	 {S. Abramsky and N. Tzevelekos},
  title = 	 {Introduction to Categories and Categorical Logic},
  note = 	 {\url{https://arxiv.org/pdf/1102.1313.pdf}},
  year = 	 {2011},
}


% (find-books "__cats/__cats.el" "baez-shulman")
%
@Unpublished{BaezShulman2007,
  author = 	 {J. Baez and M. Shulman},
  title = 	 {Lectures on $n$-Categories and Cohomology},
  note = 	 {\url{https://arxiv.org/pdf/math/0608420.pdf}},
  year = 	 {2007},
}

% (find-books "__cats/__cats.el" "lawvere-rosebrugh")
%
@Book{LawvereRosebrugh,
  author = 	 {W. Lawvere and R. Rosebrugh},
  title = 	 {Sets for Mathematics},
  publisher = 	 {Cambridge},
  year = 	 {2003},
}

% (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},
}

% (find-books "__logic/__logic.el" "van_dalen")
@Book{VanDalen,
  author = 	 {D. van Dalen},
  title = 	 {Logic and Structure (4th ed.)},
  publisher = 	 {Springer},
  year = 	 {2008},
}





% (find-es "haskell" "haskell-to-core")
%
@Unpublished{HaskellCore,
  author = 	 {V. Zavialov},
  title = 	 {Haskell to Core: Understanding Haskell Features Through Their Desugaring},
  note = 	 {\url{https://youtu.be/fty9QL4aSRc}},
  year = 	 {2020},
}

% (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},
}

% (find-books "__cats/__cats.el" "sommaruga")
%
@Book{Sommaruga,
  author = 	 {G. Sommaruga},
  title = 	 {History and Philosophy of Constructive Type Theory},
  publisher = 	 {Springer},
  year = 	 {2000},
}

% (find-books "__comp/__comp.el" "pierce")
%
@Book{Pierce,
  author = 	 {B. Pierce},
  title = 	 {Types and Programming Languages},
  publisher = 	 {MIT},
  year = 	 {2002},
}

% (find-books "__cats/__cats.el" "bauer-gddtt")
%
@Unpublished{BauerGDDTT,
  author = 	 {A. Bauer and P.G. Haselwarter and P.L. Lumsdaine},
  title = 	 {A General Definition of Dependent Type Theories},
  note = 	 {\url{https://arxiv.org/pdf/2009.05539.pdf}},
  year = 	 {2020},
}

% (find-books "__comp/__comp.el" "haskell-hutton")
%
@Book{Hutton,
  author = 	 {G. Hutton},
  title = 	 {Programming in Haskell, 2nd ed},
  publisher = 	 {Cambridge},
  year = 	 {2016},
}

% (find-books "__cats/__cats.el" "lindenhovius-gtop")
%
@Unpublished{Lindenhovius,
  author = 	 {A.J. Lindenhovius},
  title = 	 {Grothendieck Topologies on Posets},
  note = 	 {\url{https://arxiv.org/pdf/1405.4408v2.pdf}},
  year = 	 {2014},
}

% (linfp 1 "title")
% (linfa   "title")
%
@Unpublished{LindenhoviusOchs,
  author = 	 {E. Ochs},
  title = 	 {On a formula that is not in ``Grothendieck Topologies in Posets''},
  note = 	 {\url{https://arxiv.org/abs/2107.08501}},
  year = 	 {2021},
}



% (find-books "__etc/__etc.el" "pinkflag")
%
@Book{PinkFlag,
  author = 	 {W. Neate},
  title = 	 {Wire's ``Pink Flag''},
  publisher = 	 {Continuum},
  year = 	 {2008},
  series = 	 {33 1/3},
}

@Unpublished{Buzzard2021,
  author = 	 {K. Buzzard},
  title = 	 {Formalising mathematics: an introduction},
  note = 	 {\url{https://xenaproject.wordpress.com/2021/01/21/formalising-mathematics-an-introduction/}},
  year = 	 {2021},
}


% «bib-WadlerSMBF»  (to ".bib-WadlerSMBF")
% (find-angg ".emacs.agda" "wadler-smbf")
% "Programming Language Foundations in Agda"
% https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
% https://homepages.inf.ed.ac.uk/wadler/papers/plfa/sbmf.pdf
%
@InProceedings{WadlerSMBF,
  author = 	 {P. Wadler},
  title = 	 {Programming Language Foundations in Agda},
  booktitle =    {XXI Brazilian Symposium on Formal Methods},
  year = 	 {2018},
  note = 	 {\url{https://homepages.inf.ed.ac.uk/wadler/topics/agda.html\#sbmf}},
}


% «bib-DSLS»  (to ".bib-DSLS")
%
@Book{DSLsofMath,
  author = 	 {P. Jansson and C. Ionescu and J.-P. Bernardy},
  title = 	 {Domain-Specific Languages of Mathematics},
  publisher = 	 {College Publications},
  year = 	 {2022},
  note = 	 {\url{https://github.com/DSLsofMath/DSLsofMath}},
}

% «bib-Ganesalingam»  (to ".bib-Ganesalingam")
% (find-books "__phil/__phil.el" "ganesalingam")
%
@Book{Ganesalingam,
  author = 	 {M. Ganesalingam},
  title = 	 {The Language of Mathematics - A Linguistic and Philosophical Investigation},
  publisher = 	 {Springer},
  year = 	 {2013},
}


% «bib-HuCarette»  (to ".bib-HuCarette")
% (find-books "__cats/__cats.el" "hu-carette")
%
@Unpublished{HuCarette,
  author = 	 {J. Hu and J. Carette},
  title = 	 {Formalizing Category Theory in Agda},
  note = 	 {\url{https://arxiv.org/abs/2005.07059}},
  year = 	 {2020},
}










% Local variables:
% coding: utf-8-unix
% modes: (bibtex-mode fundamental-mode)
% end: