|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% My bibliography for Categorical Semantics & Related Stuff
% <U>pdated and <U>tf8-ed version, 2022mar10.
%
% Used by:
% (find-LATEXgrep "grep --color -nH -e catsem-u *")
% (find-LATEXfile "2017planar-has-1.tex" "catsem-u.bib")
% (find-LATEXfile "2017biblatex.tex" "catsem-u.bib")
% (find-LATEXfile "2017yoneda.tex" "catsem-u.bib")
%
% (find-angg "LATEX/catsem.bib")
% (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-pdf-page "~/LATEX/tmpbib.pdf")
% (find-pdf-text "~/LATEX/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-BarrWellsCTCS» (to "bib-BarrWellsCTCS")
% «.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-CaccamoWinskel» (to "bib-CaccamoWinskel")
% «.bib-CarnielliEpstein» (to "bib-CarnielliEpstein")
% «.bib-ChagrovZakharyaschev» (to "bib-ChagrovZakharyaschev")
% «.bib-ChengMorally» (to "bib-ChengMorally")
% «.bib-CoeckeNewStruP» (to "bib-CoeckeNewStruP")
% «.bib-CoeckePQP» (to "bib-CoeckePQP")
% «.bib-Coq» (to "bib-Coq")
% «.bib-Corfield» (to "bib-Corfield")
% «.bib-DaveyPriestley» (to "bib-DaveyPriestley")
% «.bib-Dummett» (to "bib-Dummett")
% «.bib-Eilenberg» (to "bib-Eilenberg")
% «.bib-Fitting» (to "bib-Fitting")
% «.bib-FongSpivak» (to "bib-FongSpivak")
% «.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-Gentzen» (to "bib-Gentzen")
% «.bib-GeuversPhD» (to "bib-GeuversPhD")
% «.bib-GeuversSN» (to "bib-GeuversSN")
% «.bib-Goedel» (to "bib-Goedel")
% «.bib-Goldblatt» (to "bib-Goldblatt")
% «.bib-Gratzer» (to "bib-Gratzer")
% «.bib-Gray66» (to "bib-Gray66")
% «.bib-HellerTierney» (to "bib-HellerTierney")
% «.bib-Hesseling» (to "bib-Hesseling")
% «.bib-HOTT» (to "bib-HOTT")
% «.bib-Howard» (to "bib-Howard")
% «.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-LawvereRosebrugh» (to "bib-LawvereRosebrugh")
% «.bib-LawvereSchanuel» (to "bib-LawvereSchanuel")
% «.bib-LawvereThesis» (to "bib-LawvereThesis")
% «.bib-Leinster» (to "bib-Leinster")
% «.bib-Luo» (to "bib-Luo")
% «.bib-Macbeth» (to "bib-Macbeth")
% «.bib-MacLane» (to "bib-MacLane")
% «.bib-MacLaneMoerdijk» (to "bib-MacLaneMoerdijk")
% «.bib-Mancosu» (to "bib-Mancosu")
% «.bib-MartinLof84» (to "bib-MartinLof84")
% «.bib-MarsdenCTUSD» (to "bib-MarsdenCTUSD")
% «.bib-McLarty» (to "bib-McLarty")
% «.bib-MilewskiCTFPOCaml» (to "bib-MilewskiCTFPOCaml")
% «.bib-ModalHandbook» (to "bib-ModalHandbook")
% «.bib-MoeRey» (to "bib-MoeRey")
% «.bib-NegriVonPlato» (to "bib-NegriVonPlato")
% «.bib-Ochs» (to "bib-Ochs")
% «.bib-PareSchumacher» (to "bib-PareSchumacher")
% «.bib-Pavlovic» (to "bib-Pavlovic")
% «.bib-Perrone» (to "bib-Perrone")
% «.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-Riehl» (to "bib-Riehl")
% «.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-ToHBCurry» (to "bib-ToHBCurry")
% «.bib-VanDalen» (to "bib-VanDalen")
% «.bib-WadlerGR» (to "bib-WadlerGR")
% «.bib-WadlerTfF» (to "bib-WadlerTfF")
% «.bib-WadlerPaT» (to "bib-WadlerPaT")
% «.bib-WadlerSMBF» (to "bib-WadlerSMBF")
%
% «.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-BarrWellsCTCS» (to ".bib-BarrWellsCTCS")
% (find-books "__cats/__cats.el" "barr-wells-ctcs")
%
@Book{BarrWellsCTCS,
author = {M. Barr and C. Wells},
title = {Category Theory for Computing Science},
publisher = {TAC Reprints},
year = {2012},
}
% «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")
% (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-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-CaccamoWinskel» (to ".bib-CaccamoWinskel")
% (find-books "__cats/__cats.el" "caccamo-winskel")
%
@Unpublished{CaccamoWinskel,
author = {M. J. Caccamo 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-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-ChagrovZakharyaschev» (to ".bib-ChagrovZakharyaschev")
% (find-books "__logic/__logic.el" "chagrov")
%
@Book{ChagrovZakharyaschev,
author = {A. Chagrov and M. Zakharyaschev},
title = {Modal Logic},
publisher = {Oxford},
year = {1997},
}
% «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-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-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-Dummett» (to ".bib-Dummett")
% (find-books "__logic/__logic.el" "dummett")
@Book{Dummett,
author = {M. Dummett},
title = {Elements of Intuitionism (2nd ed.)},
publisher = {Oxford},
year = {2000},
}
% «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-Fitting» (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 = {4},
}
% «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}},
}
% «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-books "__cats/__cats.el" "freyd76")
% (find-books "__cats/__cats.el" "heller-tierney")
% (find-angg ".emacs.papers" "freyd")
% http://angg.twu.net/scans/freyd76__properties_invariant_within_equivalence_types_of_categories.pdf
%
@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-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},
}
% «bib-Gentzen» (to ".bib-Gentzen")
% (find-books "__logic/__logic.el" "gentzen")
%
@Book{GentzenCollected,
author = {G. Gentzen},
editor = {M. E. Szabo},
title = {The Collected Papers of Gerhard Gentzen},
publisher = {North-Holland},
year = {1969},
}
% «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. Gödel},
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-Goldblatt» (to ".bib-Goldblatt")
% (find-books "__cats/__cats.el" "goldblatt")
@Book{Goldblatt,
title={Topoi: The Categorial Analysis of Logic},
author={Goldblatt, R.},
publisher={North Holland},
year={1984},
% publisher={Dover Publications},
% year={2006},
% isbn={9780486450261},
% lccn={2005046778},
% series={Dover Books on Mathematics},
% url={https://books.google.com.br/books?id=AwLc-12-7LMC}
}
% «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-Gray66» (to ".bib-Gray66")
% (find-books "__cats/__cats.el" "gray")
%
@InProceedings{Gray66,
author = {J.W. Gray},
title = {Fibred and Cofibred Categories},
booktitle = {Proceedings of the Conference on Categorical Algebra},
pages = {21--83},
year = {1966},
editor = {S. Eilenberg and D.K. Harrison and S. MacLane and H. Röhrl},
publisher = {Springer},
}
% «bib-HellerTierney» (to ".bib-HellerTierney")
% (to "bib-Freyd76")
% (find-books "__cats/__cats.el" "heller-tierney")
% 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-Hesseling» (to ".bib-Hesseling")
% (find-books "__logic/__logic.el" "hesseling")
%
@book{Hesseling,
title = {Gnomes in the Fog: The Reception of Brouwer’s Intuitionism in the 1920s},
author = {Dennis E. Hesseling (auth.)},
publisher = {Birkhäuser Basel},
year = {2003},
series = {Science Networks. Historical Studies 28},
edition = {1},
volume = {},
}
% «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 = {\url{https://homotopytypetheory.org/book}},
address = {Institute for Advanced Study},
year = {2013},
}
% «bib-Howard» (to ".bib-Howard")
% In: (find-LATEX "catsem-u.bib" "bib-ToHBCurry")
% (find-books "__logic/__logic.el" "howard")
% (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.
% «bib-HylandPitts» (to ".bib-HylandPitts")
% (find-books "__cats/__cats.el" "hyland-pitts")
% 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")
% 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")
% (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},
}
% Variants with shorthands:
%
@Book{EA,
author = {P. T. Johnstone},
title = {Sketches of an Elephant: A Topos Theory Compendium},
publisher = {Oxford University Press},
volume = {1},
% chapter = {A},
shorthand = {E},
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-books "__cats/__cats.el" "lawvere-adjfo")
% (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-equahyp")
%
@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-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-LawvereSchanuel» (to ".bib-LawvereSchanuel")
% (find-books "__cats/__cats.el" "lawvere-schanuel")
%
@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-Leinster» (to ".bib-Leinster")
% (find-books "__cats/__cats.el" "leinster-basic")
%
@Book{Leinster,
author = {T. Leinster},
title = {Basic Category Theory},
publisher = {Cambridge},
year = {2014},
}
% «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},
}
@Book{CWM2,
author = {S. MacLane},
title = {Categories for the Working Mathematician (2nd ed.)},
publisher = {Springer},
year = {1997},
}
% «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-Mancosu» (to ".bib-Mancosu")
% (find-books "__phil/__phil.el" "mancosu")
@Book{Mancosu,
editor = {P. Mancosu},
title = {The Philosophy of Mathematical Practice},
publisher = {Oxford},
year = {2008},
}
% «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-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-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-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-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-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-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
% https://doi.org/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 = {9},
volume = {7},
number = {3},
pages = {291--321},
}
@Article{OchsPH1,
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{OchsPH1,
% author = {E. Ochs},
% title = {Planar Heyting Algebras for Children},
% note = {\url{http://angg.twu.net/math-b.html\#zhas-for-children-2}},
% shorthand = {PH1},
% % year = {2017},
% year = {2020},
% }
@Unpublished{OchsPH2,
author = {E. Ochs},
title = {Planar Heyting Algebras for Children 2: Local
Operators, J-Operators, and Slashings},
note = {\url{http://angg.twu.net/math-b.html\#zhas-for-children-2}},
shorthand = {PH2},
year = {2020},
}
% (find-math-b-links "missing-diagrams-elephant" "2019oxford-abs")
@Unpublished{OchsACT2019,
author = {E. Ochs},
title = {On some missing diagrams in the Elephant},
note = {\url{http://angg.twu.net/LATEX/2019oxford-abs.pdf}},
year = {2019},
}
% (find-math-b-links "notes-yoneda" "2019notes-yoneda")
@Unpublished{OchsNotesOnYoneda,
author = {E. Ochs},
title = {A diagram for the Yoneda Lemma (In which each node
and arrow can be interpreted precisely as a
``term'', and most of the interpretations are
``obvious''; plus dictionaries!!!)},
note = {\url{http://angg.twu.net/LATEX/2019notes-yoneda.pdf}},
year = {2019},
}
@Unpublished{OchsCla2020,
author = {E. Ochs},
title = {Notes about classifiers and local operators in a
$\mathbf{Set}^{(P,A)}$},
note = {\url{http://angg.twu.net/math-b.html\#zhas-for-children-2}},
year = {2020},
}
@Unpublished{OchsLessMS,
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},
}
% (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-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-PareSchumacher» (to ".bib-PareSchumacher")
% (find-books "__cats/__cats.el" "pare-schumacher")
%
@InProceedings{PareSchumacher,
author = {R. Paré and D. Schumacher},
title = {Abstract Families and the Adjoint Functor Theorems},
booktitle = {Indexed Categories and Their Applications},
pages = {1--125},
editor = {P.T. Johnstone and R. Paré},
publisher = {Springer},
series = {Lecture Notes in Mathematics},
number = {661},
year = {1978},
}
% «bib-Pavlovic» (to ".bib-Pavlovic")
%
@PhdThesis{Pavlovic,
author = {D. Pavlovi\'c},
title = {Predicates and Fibrations},
school = {University of Utrecht},
year = {1990},
}
% «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 = {https://arxiv.org/abs/1912.10642},
year = {2020},
}
% «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},
note = {\url{https://marieetgonzalo.files.wordpress.com/2004/06/generic-figures.pdf}},
}
% «bib-Riehl» (to ".bib-Riehl")
% (find-books "__cats/__cats.el" "riehl")
@Book{Riehl,
author = {E. Riehl},
title = {Category Theory in Context},
publisher = {Dover},
year = {2016},
}
% «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-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}
}
% «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-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},
}
% «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-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-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-WadlerGR» (to ".bib-WadlerGR")
% (find-angg ".emacs.papers" "wadler-gr")
% 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).
% (find-angg ".emacs.papers" "wadler-free")
%
@InProceedings{WadlerTfF,
author = {P. Wadler},
title = {Theorems for Free!},
booktitle = {Proc. FPCA'89},
pages = {347--359},
year = {1989},
publisher = {ACM},
}
% «bib-WadlerPaT» (to ".bib-WadlerPaT")
% http://homepages.inf.ed.ac.uk/wadler/topics/history.html#propositions-as-types
% Philip Wadler. Communications of the ACM, 58(12):75–84, December, 2015.
% (find-angg ".emacs.papers" "wadler-pat")
%
@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},
}
% «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-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: utf-8-unix
% modes: (bibtex-mode fundamental-mode)
% end: