|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% This file:
% http://angg.twu.net/LATEX/catsem-ab.bib.html
% http://angg.twu.net/LATEX/catsem-ab.bib
% (find-angg "LATEX/catsem-ab.bib")
% Author: Eduardo Ochs <eduardoochs@gmail.com>
%
% The bibliography file - in Biber format - for my chapter in the
% Abduction book.
%
% See:
% (find-angg "LUA/bib.lua")
% (find-angg "LATEX/catsem-u.bib")
% (find-angg "LATEX/catsem-slides.bib")
% «.bib-AbramskyTzevelekos» (to "bib-AbramskyTzevelekos")
% «.bib-AgdaUserManual» (to "bib-AgdaUserManual")
% «.bib-Automath» (to "bib-Automath")
% «.bib-Awodey» (to "bib-Awodey")
% «.bib-BadiouLoW» (to "bib-BadiouLoW")
% «.bib-BadiouMoTT» (to "bib-BadiouMoTT")
% «.bib-BaezShulman2007» (to "bib-BaezShulman2007")
% «.bib-BauerGDDTT» (to "bib-BauerGDDTT")
% «.bib-BellLST» (to "bib-BellLST")
% «.bib-Brady» (to "bib-Brady")
% «.bib-Buzzard2021» (to "bib-Buzzard2021")
% «.bib-CWM2» (to "bib-CWM2")
% «.bib-CaccamoPhD» (to "bib-CaccamoPhD")
% «.bib-CaccamoWinskel» (to "bib-CaccamoWinskel")
% «.bib-CarsonSappho» (to "bib-CarsonSappho")
% «.bib-ChengMorally» (to "bib-ChengMorally")
% «.bib-ClopsAndTops» (to "bib-ClopsAndTops")
% «.bib-CoeckeNewStruP» (to "bib-CoeckeNewStruP")
% «.bib-CoeckePQP» (to "bib-CoeckePQP")
% «.bib-Corfield» (to "bib-Corfield")
% «.bib-DSLsofMath» (to "bib-DSLsofMath")
% «.bib-DaveyPriestley» (to "bib-DaveyPriestley")
% «.bib-Eev2019» (to "bib-Eev2019")
% «.bib-EilenbergSteenrod» (to "bib-EilenbergSteenrod")
% «.bib-Elephant1» (to "bib-Elephant1")
% «.bib-Emacs81» (to "bib-Emacs81")
% «.bib-FaiF» (to "bib-FaiF")
% «.bib-FavC» (to "bib-FavC")
% «.bib-FongSpivak» (to "bib-FongSpivak")
% «.bib-Fourman» (to "bib-Fourman")
% «.bib-Freyd76» (to "bib-Freyd76")
% «.bib-FreydAspects» (to "bib-FreydAspects")
% «.bib-FreydScedrov» (to "bib-FreydScedrov")
% «.bib-GLT» (to "bib-GLT")
% «.bib-Ganesalingam» (to "bib-Ganesalingam")
% «.bib-GirardBlind» (to "bib-GirardBlind")
% «.bib-Hazratpour» (to "bib-Hazratpour")
% «.bib-HOTT» (to "bib-HOTT")
% «.bib-HaskellCore» (to "bib-HaskellCore")
% «.bib-HuCarette» (to "bib-HuCarette")
% «.bib-Hutton» (to "bib-Hutton")
% «.bib-IDARCT» (to "bib-IDARCT")
% «.bib-IdrisCT2019» (to "bib-IdrisCT2019")
% «.bib-Jacobs» (to "bib-Jacobs")
% «.bib-Jamnik» (to "bib-Jamnik")
% «.bib-Johnstone» (to "bib-Johnstone")
% «.bib-Kamareddine» (to "bib-Kamareddine")
% «.bib-Kromer» (to "bib-Kromer")
% «.bib-KromerSlides» (to "bib-KromerSlides")
% «.bib-LambekScott» (to "bib-LambekScott")
% «.bib-LawvereRosebrugh» (to "bib-LawvereRosebrugh")
% «.bib-Leinster» (to "bib-Leinster")
% «.bib-LessMS» (to "bib-LessMS")
% «.bib-Lindenhovius» (to "bib-Lindenhovius")
% «.bib-LindenhoviusOchs» (to "bib-LindenhoviusOchs")
% «.bib-MDE» (to "bib-MDE")
% «.bib-MacLaneMoerdijk» (to "bib-MacLaneMoerdijk")
% «.bib-MacLaneNotes» (to "bib-MacLaneNotes")
% «.bib-MarsdenCTUSD» (to "bib-MarsdenCTUSD")
% «.bib-MartinLof84» (to "bib-MartinLof84")
% «.bib-MartinLofCMCP» (to "bib-MartinLofCMCP")
% «.bib-McLarty» (to "bib-McLarty")
% «.bib-MilewskiCTFPOCaml» (to "bib-MilewskiCTFPOCaml")
% «.bib-MissingAgda» (to "bib-MissingAgda")
% «.bib-NederpeltGeuvers» (to "bib-NederpeltGeuvers")
% «.bib-NegriVonPlato» (to "bib-NegriVonPlato")
% «.bib-Norell08» (to "bib-Norell08")
% «.bib-Norell09» (to "bib-Norell09")
% «.bib-OchsLucatelli» (to "bib-OchsLucatelli")
% «.bib-OchsMis1» (to "bib-OchsMis1")
% «.bib-OchsMisB» (to "bib-OchsMisB")
% «.bib-OchsTallinnAbs» (to "bib-OchsTallinnAbs")
% «.bib-OchsVGMS2018» (to "bib-OchsVGMS2018")
% «.bib-OchsWLD2019» (to "bib-OchsWLD2019")
% «.bib-PH1» (to "bib-PH1")
% «.bib-PH2» (to "bib-PH2")
% «.bib-PenroseSIGGRAPH2020» (to "bib-PenroseSIGGRAPH2020")
% «.bib-Perrone» (to "bib-Perrone")
% «.bib-Pierce» (to "bib-Pierce")
% «.bib-PinkFlag» (to "bib-PinkFlag")
% «.bib-PowerPasting» (to "bib-PowerPasting")
% «.bib-Prawitz65» (to "bib-Prawitz65")
% «.bib-Riehl» (to "bib-Riehl")
% «.bib-SICP» (to "bib-SICP")
% «.bib-SeelyBeck» (to "bib-SeelyBeck")
% «.bib-SeelyDiff» (to "bib-SeelyDiff")
% «.bib-SeelyLCCC» (to "bib-SeelyLCCC")
% «.bib-SeelyPLC» (to "bib-SeelyPLC")
% «.bib-SelingerSurveyGL» (to "bib-SelingerSurveyGL")
% «.bib-SelingerLN» (to "bib-SelingerLN")
% «.bib-Sommaruga» (to "bib-Sommaruga")
% «.bib-Taylor» (to "bib-Taylor")
% «.bib-ThompsonGardner» (to "bib-ThompsonGardner")
% «.bib-ToHBCurry» (to "bib-ToHBCurry")
% «.bib-VanBenthemJutting77» (to "bib-VanBenthemJutting77")
% «.bib-VanDalen» (to "bib-VanDalen")
% «.bib-WadlerPLFA» (to "bib-WadlerPLFA")
% «.bib-WadlerPaT» (to "bib-WadlerPaT")
% «.bib-WadlerSMBF» (to "bib-WadlerSMBF")
% «.bib-WiedjikDBF» (to "bib-WiedjikDBF")
% «bib-AbramskyTzevelekos» (to ".bib-AbramskyTzevelekos")
% (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},
}
% «bib-AgdaUserManual» (to ".bib-AgdaUserManual")
% (find-angg ".emacs.agda" "user-manual")
%
@Manual{AgdaUserManual,
title = {Agda User Manual},
author = {The Agda Team},
shorthand = {AgdaMan},
% OPTyear = {},
% OPTnote = {},
% OPTannote = {}
}
% «bib-Automath» (to ".bib-Automath")
% (find-books "__logic/__logic.el" "automath")
% See: (to "bib-VanBenthemJutting77")
%
@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")
%
@Book{Awodey,
author = {S. Awodey},
title = {Category Theory},
publisher = {Oxford},
year = {2006},
}
% «bib-BadiouLoW» (to ".bib-BadiouLoW")
% (find-books "__cats/__cats.el" "badiou-low")
%
@Book{BadiouLoW,
author = {A. Badiou},
title = {Logics of Worlds - Being and Event, 2},
publisher = {Continuum},
year = {2009},
}
% «bib-BadiouMoTT» (to ".bib-BadiouMoTT")
% (find-books "__cats/__cats.el" "badiou-mt")
%
@Book{BadiouMoTT,
author = {A. Badiou},
title = {Mathematics of The Transcendental},
publisher = {Bloomsbury},
year = {2014},
}
% «bib-BaezShulman2007» (to ".bib-BaezShulman2007")
% (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},
}
% «bib-BauerGDDTT» (to ".bib-BauerGDDTT")
% (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},
}
% «bib-BellLST» (to ".bib-BellLST")
% (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},
}
% «bib-Brady» (to ".bib-Brady")
% (find-books "__comp/__comp.el" "brady")
%
@Book{Brady,
author = {E. Brady},
title = {Type-Driven Development With Idris},
publisher = {Manning},
year = {2017},
}
% «bib-Buzzard2021» (to ".bib-Buzzard2021")
@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-CWM2» (to ".bib-CWM2")
% (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},
}
% «bib-CaccamoPhD» (to ".bib-CaccamoPhD")
% (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}},
}
% «bib-CaccamoWinskel» (to ".bib-CaccamoWinskel")
% (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},
}
% «bib-CarsonSappho» (to ".bib-CarsonSappho")
% (find-books "__etc/__etc.el" "carson-sappho")
%
@Book{CarsonSappho,
author = {A. Carson},
title = {If Not, Winter -- Fragments of Sappho},
publisher = {Vintage Books},
year = {2003},
}
% «bib-ChengMorally» (to ".bib-ChengMorally")
% (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},
}
% «bib-ClopsAndTops» (to ".bib-ClopsAndTops")
% (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},
}
% «bib-CoeckeNewStruP» (to ".bib-CoeckeNewStruP")
% (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}},
}
% «bib-CoeckePQP» (to ".bib-CoeckePQP")
% (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},
}
% «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-DSLsofMath» (to ".bib-DSLsofMath")
% (find-books "__comp/__comp.el" "dsls-of-math")
% (find-es "math" "dslsofmath")
%
@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-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-Eev2019» (to ".bib-Eev2019")
% (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}},
}
% «bib-EilenbergSteenrod» (to ".bib-EilenbergSteenrod")
% (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},
}
% «bib-Elephant1» (to ".bib-Elephant1")
% (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},
}
% «bib-Emacs81» (to ".bib-Emacs81")
@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}},
}
% «bib-FaiF» (to ".bib-FaiF")
% (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}},
}
% «bib-FavC» (to ".bib-FavC")
% (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},
}
% «bib-FongSpivak» (to ".bib-FongSpivak")
% (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}},
}
% «bib-Fourman» (to ".bib-Fourman")
% (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},
}
% «bib-Freyd76» (to ".bib-Freyd76")
% (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},
}
% «bib-FreydAspects» (to ".bib-FreydAspects")
% (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}},
}
% «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-GLT» (to ".bib-GLT")
% (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}},
}
% «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-GirardBlind» (to ".bib-GirardBlind")
% (find-books "__logic/__logic.el" "girard-blind-spot")
%
@Book{GirardBlind,
author = {J.-Y. Girard},
title = {The Blind Spot},
publisher = {European Mathematical Society},
year = {2010},
}
% «bib-Hazratpour» (to ".bib-Hazratpour")
% (find-books "__cats/__cats.el" "hazratpour")
%
@PhdThesis{Hazratpour,
author = {S. Hazratpour},
title = {A Logical Study of Some 2-Categorical Aspects of
Topos Theory},
school = {Birmingham},
year = {2019},
}
% «bib-HOTT» (to ".bib-HOTT")
% (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-HaskellCore» (to ".bib-HaskellCore")
% (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},
}
% «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},
}
% «bib-Hutton» (to ".bib-Hutton")
% (find-books "__comp/__comp.el" "haskell-hutton")
%
@Book{Hutton,
author = {G. Hutton},
title = {Programming in Haskell, 2nd ed},
publisher = {Cambridge},
year = {2016},
}
% «bib-IDARCT» (to ".bib-IDARCT")
% (find-angg ".emacs" "idarct-preprint")
%
@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},
}
% «bib-IdrisCT2019» (to ".bib-IdrisCT2019")
@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},
}
% «bib-Jacobs» (to ".bib-Jacobs")
% (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},
}
% «bib-Jamnik» (to ".bib-Jamnik")
% (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},
}
% «bib-Johnstone» (to ".bib-Johnstone")
@Book{Johnstone,
author = {P. T. Johnstone},
title = {Topos Theory},
publisher = {Academic Press},
year = {1977},
}
% «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-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},
note = {\url{https://www.springer.com/gp/book/9783764375232}},
}
% «bib-KromerSlides» (to ".bib-KromerSlides")
% (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},
}
% «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-LawvereRosebrugh» (to ".bib-LawvereRosebrugh")
% (find-books "__cats/__cats.el" "lawvere-rosebrugh")
%
@Book{LawvereRosebrugh,
author = {W. Lawvere and R. Rosebrugh},
title = {Sets for Mathematics},
publisher = {Cambridge},
year = {2003},
}
% «bib-Leinster» (to ".bib-Leinster")
% (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}},
}
% «bib-LessMS» (to ".bib-LessMS")
@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},
}
% «bib-Lindenhovius» (to ".bib-Lindenhovius")
% (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},
}
% «bib-LindenhoviusOchs» (to ".bib-LindenhoviusOchs")
% (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},
}
% «bib-MDE» (to ".bib-MDE")
% (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},
}
% «bib-MacLaneMoerdijk» (to ".bib-MacLaneMoerdijk")
% (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},
}
% «bib-MacLaneNotes» (to ".bib-MacLaneNotes")
% (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},
}
% «bib-MarsdenCTUSD» (to ".bib-MarsdenCTUSD")
% (find-books "__cats/__cats.el" "marsden-ctusd")
%
@Unpublished{MarsdenCTUSD,
author = {D. Marsden},
title = {Category Theory Using String Diagrams},
note = {\url{https://arxiv.org/pdf/1401.7220.pdf}},
year = {2014},
}
% «bib-MartinLof84» (to ".bib-MartinLof84")
% (find-books "__logic/__logic.el" "martin-lof")
% https://github.com/michaelt/martin-lof/blob/master/bibliography.bib
%
@Book{MartinLof84,
author = {P. Martin-Löf},
title = {Intuitionistic Type Theory},
publisher = {Bibliopolis},
year = {1984},
series = {Studies in Proof Theory},
address = {Napoli}
}
% «bib-MartinLofCMCP» (to ".bib-MartinLofCMCP")
% (find-books "__logic/__logic.el" "martin-lof-cmcp")
%
@incollection{MartinLofCMCP,
Author = {P. Martin-Löf},
Booktitle = {Logic, Methodology and Philosophy of Science VI, Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science, Hannover 1979},
Editor = {L. Cohen and J. {Łoś} and H. Pfeiffer and K.-P. Podewski},
Pages = {153--175},
Publisher = {North-Holland},
Series = {Studies in Logic and the Foundations of Mathematics},
Title = {Constructive mathematics and computer programming},
% Doi = {10.1016/S0049-237X(09)70189-2},
% Url = {http://dx.doi.org/10.1016/S0049-237X(09)70189-2},
Volume = {104},
Year = {1982}
}
% «bib-McLarty» (to ".bib-McLarty")
% (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},
}
% «bib-MilewskiCTFPOCaml» (to ".bib-MilewskiCTFPOCaml")
% (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},
}
% «bib-MissingAgda» (to ".bib-MissingAgda")
% (find-TH "math-b" "favorite-conventions")
%
@Unpublished{MissingAgda,
author = {E. Ochs},
title = {On the missing diagrams in Category Theory: Agda code},
note = {Work in progress! See \url{http://angg.twu.net/math-b.html\#md}},
year = {2022},
}
% «bib-NederpeltGeuvers» (to ".bib-NederpeltGeuvers")
% (find-books "__logic/__logic.el" "nederpelt-geuvers")
%
@Book{NederpeltGeuvers,
author = {R. Nederpelt and H. Geuvers},
title = {Type Theory and Formal Proof - An Introduction},
publisher = {Cambridge},
year = {2014},
}
% «bib-NegriVonPlato» (to ".bib-NegriVonPlato")
% (find-books "__logic/__logic.el" "negri-vonplato")
%
@Book{NegriVonPlato,
author = {S. Negri and J. von Plato},
title = {Structural Proof Theory},
publisher = {Cambridge},
year = {2001},
}
% «bib-Norell08» (to ".bib-Norell08")
% (find-books "__comp/__comp.el" "agda-dtp")
%
@Unpublished{Norell08,
author = {U. Norell and J. Chapman},
title = {Dependently Typed Programming in Agda},
note = {\url{http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf}},
year = {2008},
}
% «bib-Norell09» (to ".bib-Norell09")
% (find-books "__comp/__comp.el" "norell-bo")
%
@Unpublished{Norell09,
author = {A. Bove and P. Dybjer and U. Norell},
title = {A Brief Overview of Agda - A Functional Language with Dependent Types},
note = {\url{http://www.cse.chalmers.se/~ulfn/papers/tphols09/tutorial.pdf}},
year = {2009},
}
% «bib-OchsLucatelli» (to ".bib-OchsLucatelli")
% (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},
}
% «bib-OchsMis1» (to ".bib-OchsMis1")
% (find-math-b-links "2022-md" "2022on-the-missing")
% (misp 1 "title")
% (misa "title")
%
@Unpublished{OchsMis1,
author = {E. Ochs},
title = {On the the missing diagrams in Category Theory (first-person version)},
note = {\url{https://arxiv.org/abs/2204.10630}},
year = {2022},
}
% «bib-OchsMisB» (to ".bib-OchsMisB")
% (find-math-b-links "2022-md" "2022on-the-missing")
% (misp 1 "title")
% (misa "title")
%
@InBook{OchsMisB,
author = {E. Ochs},
editor = {L. Magnani},
title = {Handbook of Abductive Cognition},
chapter = {On the the missing diagrams in Category Theory},
publisher = {Springer},
year = {2023},
pages = {697--728},
note = {\url{https://doi.org/10.1007/978-3-031-10135-9_41}},
}
% «bib-OchsTallinnAbs» (to ".bib-OchsTallinnAbs")
% (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},
}
% «bib-OchsVGMS2018» (to ".bib-OchsVGMS2018")
% (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},
}
% «bib-OchsWLD2019» (to ".bib-OchsWLD2019")
% (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},
}
% «bib-PH1» (to ".bib-PH1")
@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},
}
% «bib-PH2» (to ".bib-PH2")
@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},
}
% «bib-PenroseSIGGRAPH2020» (to ".bib-PenroseSIGGRAPH2020")
% (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},
}
% «bib-Perrone» (to ".bib-Perrone")
% (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},
}
% «bib-Pierce» (to ".bib-Pierce")
% (find-books "__comp/__comp.el" "pierce")
%
@Book{Pierce,
author = {B. Pierce},
title = {Types and Programming Languages},
publisher = {MIT},
year = {2002},
}
% «bib-PinkFlag» (to ".bib-PinkFlag")
% (find-books "__etc/__etc.el" "pinkflag")
%
@Book{PinkFlag,
author = {W. Neate},
title = {Wire's ``Pink Flag''},
publisher = {Continuum},
year = {2008},
series = {33 1/3},
}
% «bib-PowerPasting» (to ".bib-PowerPasting")
% (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}},
}
% «bib-Prawitz65» (to ".bib-Prawitz65")
@Book{Prawitz65,
author = {D. Prawitz},
title = {Natural Deduction},
publisher = {Almqvist \& Wiksell, Stockholm, Sweden},
year = {1965},
}
% «bib-Riehl» (to ".bib-Riehl")
@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},
}
% «bib-SICP» (to ".bib-SICP")
% (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},
}
% «bib-SeelyBeck» (to ".bib-SeelyBeck")
% (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}},
}
% «bib-SeelyDiff» (to ".bib-SeelyDiff")
% (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}},
}
% «bib-SeelyLCCC» (to ".bib-SeelyLCCC")
% (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}},
}
% «bib-SeelyPLC» (to ".bib-SeelyPLC")
% (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}},
}
% «bib-SelingerSurveyGL» (to ".bib-SelingerSurveyGL")
% (find-books "__cats/__cats.el" "selinger-surveygl")
%
@Unpublished{SelingerSurveyGL,
author = {P. Selinger},
title = {A Survey of Graphical Languages for Monoidal Categories},
note = {\url{https://arxiv.org/pdf/0908.3347.pdf}},
year = {2009},
}
% «bib-SelingerLN» (to ".bib-SelingerLN")
% (find-books "__cats/__cats.el" "selinger-ln")
%
@Unpublished{SelingerLN,
author = {P. Selinger},
title = {Lecture Notes on the Lambda Calculus},
note = {\url{https://arxiv.org/abs/0804.3434v2}},
year = {2013},
}
% «bib-Sommaruga» (to ".bib-Sommaruga")
% (find-books "__cats/__cats.el" "sommaruga")
%
@Book{Sommaruga,
author = {G. Sommaruga},
title = {History and Philosophy of Constructive Type Theory},
publisher = {Springer},
year = {2000},
}
% «bib-Taylor» (to ".bib-Taylor")
% (find-books "__cats/__cats.el" "taylor")
%
@Book{Taylor,
author = {P. Taylor},
title = {Practical Foundations of Mathematics},
publisher = {Cambridge},
year = {1999},
}
% «bib-ThompsonGardner» (to ".bib-ThompsonGardner")
% (find-books "__analysis/__analysis.el" "thompson-gardner")
%
@Book{ThompsonGardner,
author = {S. P. Thompson and M. Gardner},
title = {Calculus Made Easy: being a very-simplest
introduction to those beautiful methods of reckoning
which are generally called by the terrifying names
of the differential calculus and the integral
calculus},
publisher = {St. Martin's Press},
year = {1988},
}
% «bib-ToHBCurry» (to ".bib-ToHBCurry")
% Contains: (find-LATEX "catsem-u.bib" "bib-Howard")
% See: (find-angg ".emacs.papers" "wadler-pat")
% https://www.amazon.com.br/H-B-Curry-Essays-Combinatory-Calculus-Formalism/dp/0123490502
% [32] W. A. Howard. The formulae-as-types notion of construction. In
% To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus,
% and Formalism, pages 479-491. Academic Press, 1980. The original
% version was circulated privately in 1969.
%
@Book{ToHBCurry,
editor = {J. P. Seldin and J. R. Hindley},
title = {To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism},
publisher = {Academic Press},
year = {1980},
}
% «bib-VanBenthemJutting77» (to ".bib-VanBenthemJutting77")
% (find-books "__logic/__logic.el" "automath")
% (find-books "__logic/__logic.el" "automath" "701" "Checking Landau's")
% (find-angg ".emacs.papers" "biber")
% TODO: indicate that I used pages that are in:
% (to "bib-Automath")
%
@PhdThesis{VanBenthemJutting77,
author = {L. S. van Benthem Jutting},
title = {Checking Landau's `Grundlagen' in the Automath System},
school = {Eindhoven University of Technology},
year = {1977},
}
% «bib-VanDalen» (to ".bib-VanDalen")
% (find-books "__logic/__logic.el" "van_dalen")
%
@Book{VanDalen,
author = {D. van Dalen},
title = {Logic and Structure (4th ed.)},
publisher = {Springer},
year = {2008},
}
% «bib-WadlerPLFA» (to ".bib-WadlerPLFA")
% (find-angg ".emacs.agda" "plfa-chapters")
% https://plfa.inf.ed.ac.uk/Citing/
%
@Book{WadlerPLFA,
author = {P. Wadler and W. Kokke and J. G. Siek},
title = {Programming Language Foundations in {A}gda},
year = {2020},
month = jul,
url = {http://plfa.inf.ed.ac.uk/20.07/},
}
% «bib-WadlerPaT» (to ".bib-WadlerPaT")
%
@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},
}
% «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-WiedjikDBF» (to ".bib-WiedjikDBF")
% (find-books "__logic/__logic.el" "wiedijk-dbf")
%
@Unpublished{WiedjikDBF,
author = {F. Wiedijk},
title = {The De Bruijn Factor},
note = {\url{https://www.cs.ru.nl/~freek/factor/factor.pdf}},
year = {2000},
}
% Local variables:
% coding: utf-8-unix
% modes: (bibtex-mode fundamental-mode)
% end: