.emacs.papers (htmlized)

Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
;; This file:
;;    http://angg.twu.net/.emacs.papers
;;    http://angg.twu.net/.emacs.papers.html
;; file:///home/edrx/TH/L/.emacs.papers.html
;; (find-angg ".emacs.papers")

;; (find-angg ".emacs")
;; (find-angg ".emacs" ".emacs.papers")
;; (find-angg ".emacs" "find-xxxpage")
;; (find-angg ".emacs" "papers")
;; (find-TH "eev-article")

;; «.find-pdfpage»	(to "find-pdfpage")
;; «.code-pdf»		(to "code-pdf")

;; «.abel»		(to "abel")
;; «.avigad»		(to "avigad")
;; «.awodey»		(to "awodey")
;; «.barendregt»	(to "barendregt")
;; «.barr»		(to "barr")
;; «.beck»		(to "beck")
;; «.beeson»		(to "beeson")
;; «.blass»		(to "blass")
;; «.blute»		(to "blute")
;; «.butz»		(to "butz")
;; «.cheng»		(to "cheng")
;; «.depaiva»		(to "depaiva")
;; «.dybjer»		(to "dybjer")
;; «.eliasson»		(to "eliasson")
;; «.farmer»		(to "farmer")
;; «.fiore»		(to "fiore")
;; «.freyd»		(to "freyd")
;; «.geuvers»		(to "geuvers")
;; «.girard»		(to "girard")
;; «.goedel»		(to "goedel")
;; «.grothendieck»	(to "grothendieck")
;; «.gurevich»		(to "gurevich")
;; «.hatcher»		(to "hatcher")
;; «.henkin»		(to "henkin")
;; «.hoare»		(to "hoare")
;; «.hodges»		(to "hodges")
;; «.hofmann»		(to "hofmann")
;; «.jacobs»		(to "jacobs")
;; «.jibladze»		(to "jibladze")
;; «.joao_marcos»	(to "joao_marcos")
;; «.johnstone»		(to "johnstone")
;; «.kanovei»		(to "kanovei")
;; «.keisler»		(to "keisler")
;; «.kelly»		(to "kelly")
;; «.kock»		(to "kock")
;; «.kondratiev»	(to "kondratiev")
;; «.lamport»		(to "lamport")
;; «.lawvere»		(to "lawvere")
;; «.leinster»		(to "leinster")
;; «.levy»		(to "levy")
;; «.luo»		(to "luo")
;; «.martin-lof»	(to "martin-lof")
;; «.mckinsey»		(to "mckinsey")
;; «.moerdijk»		(to "moerdijk")
;; «.moggi»		(to "moggi")
;; «.nelson»		(to "nelson")
;; «.palmgren»		(to "palmgren")
;; «.pastro»		(to "pastro")
;; «.phoa»		(to "phoa")
;; «.pitts»		(to "pitts")
;; «.reynolds»		(to "reynolds")
;; «.rosolini»		(to "rosolini")
;; «.schalk»		(to "schalk")
;; «.seely»		(to "seely")
;; «.shulman»		(to "shulman")
;; «.simmons»		(to "simmons")
;; «.simpson»		(to "simpson")
;; «.street»		(to "street")
;; «.streicher»		(to "streicher")
;; «.taylor»		(to "taylor")
;; «.troelstra»		(to "troelstra")
;; «.vistoli»		(to "vistoli")
;; «.wadler»		(to "wadler")
;; «.winskel»		(to "winskel")
;; «.yanofsky»		(to "yanofsky")

;; «.coetzee»		(to "coetzee")
;; «.bentley»		(to "bentley")
;; «.nassopoulos»	(to "nassopoulos")
;; «.profsoftdevel»	(to "profsoftdevel")
;; «.tesemestr»		(to "tesemestr")
;; «.weber»		(to "weber")

;; «.lua»		(to "lua")
;; «.bibtex»		(to "bibtex")
;; «.memoirclass»	(to "memoirclass")
;; «.symbols»		(to "symbols")
;; «.texbook»		(to "texbook")
;; «.mfbook»		(to "mfbook")
;; «.texbytopic»	(to "texbytopic")
;; «.lshort»		(to "lshort")
;; «.diagxy»		(to "diagxy")
;; «.xfig»		(to "xfig")
;; «.postscript»	(to "postscript")
;; «.coq»		(to "coq")
;; «.ruby»		(to "ruby")
;; «.ruby-pragmatic»	(to "ruby-pragmatic")

;; «.rmsessays»		(to "rmsessays")


(defun +/2 (a b)
  (floor (+ a (/ b 2.0))))



;; «find-pdfpage»  (to ".find-pdfpage")
;; (find-anggfile ".emacs" "defun code-pdftotext")
;; (find-eev "eev.el" "find-xpdfpage")
;;
;; «code-pdf»  (to ".code-pdf")
;; (find-eev "eev.el" "code-xpdf")
;;
;; An example of usage:
;; (eev     "psne http://www.tannerlectures.utah.edu/lectures/documents/Coetzee99.pdf")
;; (find-pspage "$S/http/www.tannerlectures.utah.edu/lectures/documents/Coetzee99.pdf")
;; (code-ps        "livesofanimals" "$S/http/www.tannerlectures.utah.edu/lectures/documents/Coetzee99.pdf")
;; (code-pdftotext "livesofanimals" "$S/http/www.tannerlectures.utah.edu/lectures/documents/Coetzee99.pdf")
;; (find-livesofanimalspage 1)
;; (find-livesofanimalstext)
;; (find-livesofanimalspage (+ -110 147) "Rilke's panther")
;; (find-livesofanimalstext        "147" "Rilke's panther")
;; "The jaguar's vision, unlike the panther's, is not blunted. On the
;; contrary, his eyes drill through the darkness of space. The cage
;; has no reality to him, he is elsewhere."



;; «avigad»  (to ".avigad")
;; Avigad/Helzner:
;; "Transfer principles in nonstandard intuitionistic arithmetic"
;; http://www.andrew.cmu.edu/user/avigad/papers.html
;; http://www.andrew.cmu.edu/user/avigad/Papers/nonstandard.dvi
;; http://www.andrew.cmu.edu/user/avigad/Papers/nonstandard.pdf
(code-dvi       "avigadtr" "$S/http/www.andrew.cmu.edu/user/avigad/Papers/nonstandard.dvi")
(code-pdftotext "avigadtr" "$S/http/www.andrew.cmu.edu/user/avigad/Papers/nonstandard.pdf")
;; (find-avigadtrpage 1)
;; (find-avigadtrpage 19 "Transfer principles")
;; (find-avigadtrtext)

;; «abel»  (to ".abel")
;; Andreas Abel:
;; "A Semantic Analysis of Structural Recursion" (1999):
;;   http://www.tcs.informatik.uni-muenchen.de/~abel/diplomathesis.dvi
;; "Introduction to Parigot's lambda-mu-Calculus" (2001):
;;   http://www.tcs.informatik.uni-muenchen.de/~abel/parigot.ps.gz
;; "A Polymorphic Lambda-Calculus with Sized Higher-Order Types" (2006):
;;   http://www.tcs.informatik.uni-muenchen.de/~abel/diss.dvi
;; (find-sh "cd $S/http/www.tcs.informatik.uni-muenchen.de/~abel/ && dvipdf diplomathesis.dvi")
;; (find-sh "cd $S/http/www.tcs.informatik.uni-muenchen.de/~abel/ && zcat parigot.ps.gz | ps2pdf - parigot.pdf")
;; (find-sh "cd $S/http/www.tcs.informatik.uni-muenchen.de/~abel/ && dvipdf diss.dvi")
(code-dvi       "abelsr" "$S/http/www.tcs.informatik.uni-muenchen.de/~abel/diplomathesis.dvi")
(code-pdftotext "abelsr" "$S/http/www.tcs.informatik.uni-muenchen.de/~abel/diplomathesis.pdf")
(code-ps        "abelparigot" "$S/http/www.tcs.informatik.uni-muenchen.de/~abel/parigot.ps.gz")
(code-pdftotext "abelparigot" "$S/http/www.tcs.informatik.uni-muenchen.de/~abel/parigot.pdf")
(code-dvi       "abelplchot" "$S/http/www.tcs.informatik.uni-muenchen.de/~abel/diss.dvi")
(code-pdftotext "abelplchot" "$S/http/www.tcs.informatik.uni-muenchen.de/~abel/diss.pdf")
;; (find-abelsrpage 1)
;; (find-abelsrtext)
;; (find-abelparigotpage 1)
;; (find-abelparigottext)
;; (find-abelplchotpage 1)
;; (find-abelplchottext)


;; «awodey»  (to ".awodey")
;; Awodey/Warren 2007: "Homotopy Theoretic Models of Identity Types"
;;   http://www.andrew.cmu.edu/user/awodey/
;;   http://www.andrew.cmu.edu/user/mwarren/
;;   http://www.andrew.cmu.edu/~mwarren/Papers/hmit.pdf
;; "Logic in Topoi: Functorial Semantics for Higher-Order Logic" (thesis):
;;   http://www.andrew.cmu.edu/user/awodey/thesis/thesis.ps.gz
;; Notes on Algebraic Set Theory
;;   http://www.phil.cmu.edu/projects/ast/
;;   http://www.phil.cmu.edu/projects/ast/Papers/bnotes.pdf
;; (find-sh "cd $S/http/www.andrew.cmu.edu/user/awodey/thesis/ && zcat thesis.ps.gz | ps2pdf - thesis.pdf")
(code-ps        "hmit" "$S/http/www.andrew.cmu.edu/~mwarren/Papers/hmit.pdf")
(code-pdftotext "hmit" "$S/http/www.andrew.cmu.edu/~mwarren/Papers/hmit.pdf")
(code-ps        "awodeythesis" "$S/http/www.andrew.cmu.edu/user/awodey/thesis/thesis.ps.gz")
(code-pdftotext "awodeythesis" "$S/http/www.andrew.cmu.edu/user/awodey/thesis/thesis.pdf")
(code-ps        "awodeyastnotes" "$S/http/www.phil.cmu.edu/projects/ast/Papers/bnotes.pdf")
(code-pdftotext "awodeyastnotes" "$S/http/www.phil.cmu.edu/projects/ast/Papers/bnotes.pdf")
;; (find-hmitpage 1)
;; (find-hmittext)
;; (find-awodeythesispage 1)
;; (find-awodeythesistext)
;; (find-awodeyastnotespage 1)
;; (find-awodeyastnotestext)

;; Steve Awodey: "Category Theory" (book)
(code-xpdf      "awodeyct" "~/books/awodey_CT.pdf")
(code-pdftotext "awodeyct" "~/books/awodey_CT.pdf")
;; (find-awodeyctpage 7 "Contents")
;; (find-awodeyctpage (+ 10 251) "Index")
;; (find-awodeyctpage (+ 10 131) "7.3. Stone Duality")
;; (find-awodeyctpage (+ 10 159) "8. Categories of Diagrams")
;; (find-awodeycttext)
;; (find-awodeycttext "CONTENTS")
;; (find-awodeycttext "  INDEX\n")






;; «barendregt»  (to ".barendregt")
;; http://www.cs.ru.nl/~henk/papers.html
;; "Lambda-Calculi wity Types" (1992):
;;   ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps
;; (find-sh "cd $S/ftp/ftp.cs.ru.nl/pub/CompMath.Found/ && cat HBK.ps | ps2pdf - HBK.pdf")
(code-ps        "bdrgt" "$S/ftp/ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps")
(code-pdftotext "bdrgt" "$S/ftp/ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps")
;; (find-bdrgtpage 1)
;; (find-bdrgtpage 84 "(rules for lambda-omega)")
;; (find-bdrgttext)


;; «barr»  (to ".barr")
;; (find-es "math" "barr_wells")
;; http://www.tac.mta.ca/tac/reprints/articles/12/tr12.dvi
;; http://www.tac.mta.ca/tac/reprints/articles/12/tr12.pdf
(code-dvi       "ttt" "$S/http/www.tac.mta.ca/tac/reprints/articles/12/tr12.dvi")
(code-pdftotext "ttt" "$S/http/www.tac.mta.ca/tac/reprints/articles/12/tr12.pdf")
;; (find-tttpage 1)
;; (find-ttttext)
;; (find-tttpage (+ 13 57) "10. Filtered colimits")
;; (find-ttttext           "10. Filtered colimits")
;; More about filtered colimits in CWM, pp.207-214.

;; (find-sh0 "cp -v $S/http/www.tac.mta.ca/tac/reprints/articles/12/tr12.dvi /tmp/")
;; (eev "cd /tmp/ && dvired -D 300 -P pk -o tr12.ps tr12.dvi")
;; (find-pspage "/tmp/tr12.ps")

;; http://www.cwru.edu/artsci/math/wells/pub/dvi/tt.dvi
;; (code-dvi "ttt" "$S/http/www.cwru.edu/artsci/math/wells/pub/dvi/tt.dvi")
;; (find-tttpage (+ 14 285))





;; «beck»  (to ".beck")
;; http://www.tac.mta.ca/tac/reprints/articles/2/tr2abs.html
;; http://www.tac.mta.ca/tac/reprints/articles/2/tr2.dvi
;; http://www.tac.mta.ca/tac/reprints/articles/2/tr2.pdf
(code-dvi       "beckthesis" "$S/http/www.tac.mta.ca/tac/reprints/articles/2/tr2.dvi")
(code-pdftotext "beckthesis" "$S/http/www.tac.mta.ca/tac/reprints/articles/2/tr2.pdf")
;; (find-beckthesispage 1)
;; (find-beckthesistext)


;; «beeson»  (to ".beeson")
;; (find-angg "LATEX/filters.bib" "beeson")
;; http://michaelbeeson.com/research/papers/pubs.html
;; http://michaelbeeson.com/research/papers/nsappt.dvi
;; http://michaelbeeson.com/research/papers/LimitTheory.dvi
;; (find-sh "cd $S/http/michaelbeeson.com/research/papers/ && dvipdf nsappt.dvi")
;; (find-sh "cd $S/http/michaelbeeson.com/research/papers/ && dvipdf LimitTheory.dvi")
(code-dvi       "beesonnsaec" "$S/http/michaelbeeson.com/research/papers/nsappt.dvi")
(code-pdftotext "beesonnsaec" "$S/http/michaelbeeson.com/research/papers/nsappt.pdf")
(code-dvi       "beesonlimits" "$S/http/michaelbeeson.com/research/papers/LimitTheory.dvi")
(code-pdftotext "beesonlimits" "$S/http/michaelbeeson.com/research/papers/LimitTheory.pdf")
;; (find-beesonnsaecpage 1)
;; (find-beesonnsaectext)
;; (find-beesonnsaecpage 28 "neighborhood semantics")
;; (find-beesonnsaectext    "neighborhood semantics")
;; (find-beesonlimitspage 1)
;; (find-beesonlimitstext)
;; (find-beesonlimitstext "filters")


;; «blass»  (to ".blass")
;; (find-angg "LATEX/filters.bib" "blass")
;; http://matwbn.icm.edu.pl/ksiazki/fm/fm94/fm94115.pdf
(code-xpdf "blassfilters" "$S/http/matwbn.icm.edu.pl/ksiazki/fm/fm94/fm94115.pdf")
;; (find-blassfilterspage 1)


;; «blute»  (to ".blute")
;; http://aix1.uottawa.ca/~rblute/
;; http://aix1.uottawa.ca/~rblute/publications.html
;;
;; Category theory for linear logicians (Blute / Scott 2004):
;;   http://aix1.uottawa.ca/~rblute/catsurv.ps
;; Examples of differential categories (slides for CT07 talk):
;;   http://aix1.uottawa.ca/~rblute/diffcats.pdf
;; Differential Categories (Blute / Cockett / Seely):
;;   http://aix1.uottawa.ca/~rblute/difftl.ps
;;   see: (to "seely")
(code-ps       "blutecatsurv" "$S/http/aix1.uottawa.ca/~rblute/catsurv.ps")
(code-pstotext "blutecatsurv" "$S/http/aix1.uottawa.ca/~rblute/catsurv.ps")
;; (find-blutecatsurvpage 1)
;; (find-blutecatsurvtext)
(code-xpdf     "blutediffsl" "$S/http/aix1.uottawa.ca/~rblute/diffcats.pdf")
;; (find-blutediffslpage 1)


;; «butz»  (to ".butz")
;; Carsten Butz: "The filter construction revisited"
;; http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.1424
;; (find-sh0 "mv -iv 10.1.1.44.1424.pdf $S/http/citeseerx.ist.psu.edu/")
;; http://citeseerx.ist.psu.edu/10.1.1.44.1424.pdf
(code-ps        "butzfilter" "$S/http/citeseerx.ist.psu.edu/10.1.1.44.1424.pdf")
(code-pdftotext "butzfilter" "$S/http/citeseerx.ist.psu.edu/10.1.1.44.1424.pdf")
;; (find-butzfilterpage 1)
;; (find-butzfiltertext)

;; http://citeseer.ist.psu.edu/197614.html
;; (find-fline "~/tmp/the-filter-construction-revisited.pdf")
;; (code-ps        "butzfilter" "~/tmp/the-filter-construction-revisited.pdf")
;; (code-pdftotext "butzfilter" "~/tmp/the-filter-construction-revisited.pdf")
;; (find-butzfilterpage 1)
;; (find-butzfiltertext)
;; (code-ps "butzfilter" "$S/http/www.brics.dk/~butz/public_ftp/new_stuff/filter.ps.gz")
;; (code-ps "butzm"      "$S/http/www.brics.dk/~butz/public_ftp/new_stuff/butz-moerdijk.ps.gz")
;; (find-butzfilterpage 1)
;; (find-butzmpage 1)

;; «cheng»  (to ".cheng")
;; http://www.cheng.staff.shef.ac.uk/
;; http://cheng.staff.shef.ac.uk/morality/
;; http://cheng.staff.shef.ac.uk/morality/morality.pdf
(code-ps        "chengmorality" "$S/http/cheng.staff.shef.ac.uk/morality/morality.pdf")
(code-xpdf      "chengmorality" "$S/http/cheng.staff.shef.ac.uk/morality/morality.pdf")
(code-pdftotext "chengmorality" "$S/http/cheng.staff.shef.ac.uk/morality/morality.pdf")
;; (find-chengmoralitypage 1)
;; (find-chengmoralitytext)



;; «depaiva»  (to ".depaiva")
;; Gavin Bierman/Valéria de Paiva: "On an Intuitionistic Modal Logic"
;; http://www.cs.bham.ac.uk/~vdp/publications/studia.ps.gz
;; (find-sh "cd $S/http/www.cs.bham.ac.uk/~vdp/publications/ && zcat studia.ps.gz | ps2pdf - studia.pdf")
(code-ps        "vdpiml" "$S/http/www.cs.bham.ac.uk/~vdp/publications/studia.ps.gz")
(code-pdftotext "vdpiml" "$S/http/www.cs.bham.ac.uk/~vdp/publications/studia.pdf")
;; (find-vdpimlpage 1)
;; (find-vdpimltext)
;; (find-LTX "2008modallogic")

;; Alechina/Mendler/dePaiva/Ritter:
;; "Categorical and Kripke Semantics for Constructive S4 Modal Logic"
;; http://www.cs.nott.ac.uk/~nza/valeria.pdf
(code-ps        "vdpnamm" "$S/http/www.cs.nott.ac.uk/~nza/valeria.pdf")
(code-pdftotext "vdpnamm" "$S/http/www.cs.nott.ac.uk/~nza/valeria.pdf")
;; (find-vdpnammpage 1)
;; (find-vdpnammtext)



;; VdPaiva: Lineales
;; http://www2.parc.com/spl/members/paiva/publications/llc8.ps



;; «dybjer»  (to ".dybjer")
;; Peter Dybjer 1995: "Internal Type Theory"
;;   http://www.cs.chalmers.se/~peterd/papers/InternalTT.ps
;; Cubric/Dybjer/Scott: "Normalization and the Yoneda Embedding"
;;   http://www.cs.chalmers.se/~peterd/papers/Yonedaccc.ps
;; Dybjer/Buisse: "Towards Formalizing Categorical Models of Type Theory in Type Theory"
;;   http://www.cs.chalmers.se/~peterd/papers/Bremen2007.pdf
;; "(What I Know about) the History of the Identity Type" (slides, 2006):
;;   http://www.cs.chalmers.se/~peterd/papers/historyidentitytype.pdf
(code-ps        "internaltt" "$S/http/www.cs.chalmers.se/~peterd/papers/InternalTT.ps")
(code-pdftotext "internaltt" "$S/http/www.cs.chalmers.se/~peterd/papers/InternalTT.pdf")
(code-ps        "yonedaccc" "$S/http/www.cs.chalmers.se/~peterd/papers/Yonedaccc.ps")
(code-pdftotext "yonedaccc" "$S/http/www.cs.chalmers.se/~peterd/papers/Yonedaccc.pdf")
(code-ps        "catmodelstttt" "$S/http/www.cs.chalmers.se/~peterd/papers/Bremen2007.pdf")
(code-pdftotext "catmodelstttt" "$S/http/www.cs.chalmers.se/~peterd/papers/Bremen2007.pdf")
(code-xpdf      "idtype" "$S/http/www.cs.chalmers.se/~peterd/papers/historyidentitytype.pdf")
(code-pdftotext "idtype" "$S/http/www.cs.chalmers.se/~peterd/papers/historyidentitytype.pdf")
;; (find-internalttpage 1)
;; (find-internaltttext)
;; (find-yonedacccpage 1)
;; (find-yonedaccctext)
;; (find-catmodelsttttpage 1)
;; (find-catmodelstttttext)
;; (find-idtypepage 1)
;; (find-idtypetext)





;; «eliasson»  (to ".eliasson")
;; <http://www.math.uu.se/~jonase/>?
;; http://dblp.uni-trier.de/db/indices/a-tree/e/Eliasson:Jonas.html
;; http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.6032
;; http://www.math.uu.se/research/pub/FEliasson1.pdf
(code-ps        "eliasson" "$S/http/www.math.uu.se/research/pub/FEliasson1.pdf")
(code-pdftotext "eliasson" "$S/http/www.math.uu.se/research/pub/FEliasson1.pdf")
;; (find-eliassonpage 1)
;; (find-eliassontext)

;; Jonas Eliasson: Ultrasheaves. Uppsala dissertations in Mathematics 30, 2003.
;; (code-ps  "eliasson1" "$S/http/www.math.uu.se/~jonase/papers/artikel.ps")
;; (code-ps  "eliasson2" "$S/http/www.math.uu.se/~jonase/papers/artikel2.ps")
;;  (find-eliassonpage 1)
;;  (find-eliasson2page 1)



;; «farmer»  (to ".farmer")
;; William M. Farmer: The Seven Virtues of Simple Type Theory
;; http://www.cas.mcmaster.ca/sqrl/papers/sqrl18.ps.Z
(code-ps "farmer7v" "$S/http/www.cas.mcmaster.ca/sqrl/papers/sqrl18.ps.Z")
;; (find-farmer7vpage 1)


;; «fiore»  (to ".fiore")
;; "Objects of Categories as Complex Numbers" (Fiore / Leinster):
;;   http://www.arxiv.org/abs/math.CT/0212377
;; "Differential Structure in Models of...":
;;   http://www.cl.cam.ac.uk/~mpf23/papers/Types/diff.pdf
;;   Slides: http://www.cl.cam.ac.uk/~mpf23/talks/CQL2007.pdf
(code-ps        "fiorepoly" "$S/http/www.arxiv.org/abs/math.CT/0212377.pdf")
(code-pdftotext "fiorepoly" "$S/http/www.arxiv.org/abs/math.CT/0212377.pdf")
(code-ps        "fiorediff" "$S/http/www.cl.cam.ac.uk/~mpf23/papers/Types/diff.pdf")
(code-pdftotext "fiorediff" "$S/http/www.cl.cam.ac.uk/~mpf23/papers/Types/diff.pdf")
(code-ps        "fiorediffsl" "$S/http/www.cl.cam.ac.uk/~mpf23/talks/CQL2007.pdf")
(code-pdftotext "fiorediffsl" "$S/http/www.cl.cam.ac.uk/~mpf23/talks/CQL2007.pdf")
;; (find-fiorepolypage 1)
;; (find-fiorepolytext)
;; (find-fiorediffpage 1)
;; (find-fioredifftext)
;; (find-fiorediffslpage 15)
;; (find-fiorediffsltext)


;; «freyd»  (to ".freyd")
;; Freyd: Abelian Categories
;; http://www.tac.mta.ca/tac/reprints/articles/3/tr3.pdf
(code-xpdf "freydabcats" "$S/http/www.tac.mta.ca/tac/reprints/articles/3/tr3.pdf")
;; (find-freydabcatspage 1)
;; (find-freydabcatspage (+ 27 17))
;; (find-freydabcatspage (+ 27 39) "difference kernel")
;; (find-freydabcatspage (+ 27 47) "summation map")



;; «geuvers»  (to ".geuvers")
;; http://www.cs.ru.nl/~herman/PUBS/Proefschrift.ps.gz
(code-ps        "geuvthesis" "$S/http/www.cs.ru.nl/~herman/PUBS/Proefschrift.ps.gz")
(code-pdftotext "geuvthesis" "$S/http/www.cs.ru.nl/~herman/PUBS/Proefschrift.pdf")
;; (find-geuvthesispage 1)
;; (find-geuvthesistext)
;; (find-geuvthesistext    "Definition. A Pure Type System")
;; (find-geuvthesispage 76 "Definition. A Pure Type System")
;; (find-geuvthesistext    "4.3.1. The cube of typed lambda calculi")
;; (find-geuvthesispage 80 "4.3.1. The cube of typed lambda calculi")
;; (find-geuvthesistext    "The cube of logical typed lambda calculi")
;; (find-geuvthesispage 85 "The cube of logical typed lambda calculi")



;; «girard»  (to ".girard")
;; Girard/Lafont/Taylor: "Proof and Types"
;; http://www.monad.me.uk/stable/Proofs+Types.html
;; http://www.monad.me.uk/stable/prot.dvi
;; http://www.monad.me.uk/stable/prot.pdf
(code-dvi       "glt" "$S/http/www.monad.me.uk/stable/prot.dvi")
(code-pdftotext "glt" "$S/http/www.monad.me.uk/stable/prot.pdf")
;; (find-gltpage 1)
;; (find-glttext)
;; (find-gltpage (+ 8 72) "\nSums in Natural Deduction")
;; (find-glttext          "\nSums in Natural Deduction")
;; (find-gltpage (+ 8 76) "10.4. COMMUTING CONVERSIONS")
;; (find-glttext          "10.4. COMMUTING CONVERSIONS")
;; (find-gltpage (+ 8 80) "match t with inl x")
;; (find-glttext          "match t with inl x")

;; http://iml.univ-mrs.fr/~girard/cerisy.pdf
;; (find-girardcerisypage 1)
(code-ps "girardcerisy" "$S/http/iml.univ-mrs.fr/~girard/cerisy.pdf")

;; http://iml.univ-mrs.fr/~girard/linear.pdf
(code-xpdf "girardtcs" "$S/http/iml.univ-mrs.fr/~girard/linear.pdf")
;; (find-girardtcspage 1)


;; «goedel»  (to ".goedel")
;; A review of [Gödel1933f], a.k.a.:
;;   "An Interpretation of the Intuitionistic Propositional Calculus"
;; http://www.jstor.org/stable/2274984
;; http://www.jstor.org/stable/pdfplus/2274984.pdf
(code-xpdf      "godelS4rev" "$S/http/www.jstor.org/stable/pdfplus/2274984.pdf")
(code-pdftotext "godelS4rev" "$S/http/www.jstor.org/stable/pdfplus/2274984.pdf")
;; (find-godelS4revpage 1)
;; (find-godelS4revtext)



;; «grothendieck»  (to ".grothendieck")
;; (find-TH "math-b" "Grothendieck")
;; http://archive.numdam.org/
;; http://kolmogorov.unex.es/~navarro/res/
;; http://www.institut.math.jussieu.fr/~maltsin/groth/Derivateurs.html

;; http://kolmogorov.unex.es/~navarro/res/tohoku.pdf
(code-xpdf "grothtohoku" "$S/http/kolmogorov.unex.es/~navarro/res/tohoku.pdf")
;; (find-grothtohokupage 1)

;; http://www.math.jussieu.fr/~leila/grothendieckcircle/GrothKansas.pdf
(code-ps   "grothkansas" "$S/http/www.math.jussieu.fr/~leila/grothendieckcircle/GrothKansas.pdf")
(code-xpdf "grothkansas" "$S/http/www.math.jussieu.fr/~leila/grothendieckcircle/GrothKansas.pdf")
;; (find-grothkansaspage (+ 4 62))
;; (find-grothkansaspage 1)

;; The Cohomology Theory of Abstract Algebraic Varieties (1958/60)
;; http://www.math.jussieu.fr/~leila/grothendieckcircle/CohomologyVarieties.pdf
(code-ps "grothcohovar" "$S/http/www.math.jussieu.fr/~leila/grothendieckcircle/CohomologyVarieties.pdf")
;; (find-grothcohovarpage 1)

;; Fondements de la Geometrie Algebrique (1957--62)
;; http://www.math.jussieu.fr/~leila/grothendieckcircle/FGA.pdf
(code-ps   "grothfga" "$S/http/www.math.jussieu.fr/~leila/grothendieckcircle/FGA.pdf")
(code-xpdf "grothfga" "$S/http/www.math.jussieu.fr/~leila/grothendieckcircle/FGA.pdf")
;; (find-grothfgapage (+ 13 1))
;; (find-grothfgapage 1)

;; EGA I:
;; http://www.numdam.org/numdam-bin/fitem?id=PMIHES_1960__4__5_0
;;         http://archive.numdam.org/article/PMIHES_1960__4__5_0.pdf
;; EGA II:
;; http://www.numdam.org/numdam-bin/fitem?id=PMIHES_1961__8__5_0
;;         http://archive.numdam.org/article/PMIHES_1961__8__5_0.pdf
(code-xpdf "grothega1" "$S/http/archive.numdam.org/article/PMIHES_1960__4__5_0.pdf")
(code-xpdf "grothega2" "$S/http/archive.numdam.org/article/PMIHES_1961__8__5_0.pdf")
;; (find-grothega1page (+ -1 11))
;; (find-grothega2page (+ -3 5))

;; Comme Appelé du Néant -- As If Summoned from the Void:
;; The Life of Alexandre Grothendieck (Allyn Jackson, 2004)
;; http://www.ams.org/notices/200409/fea-grothendieck-part1.pdf
;; http://www.ams.org/notices/200410/fea-grothendieck-part2.pdf
(code-ps        "grothams1" "$S/http/www.ams.org/notices/200409/fea-grothendieck-part1.pdf")
(code-pdftotext "grothams1" "$S/http/www.ams.org/notices/200409/fea-grothendieck-part1.pdf")
(code-ps        "grothams2" "$S/http/www.ams.org/notices/200410/fea-grothendieck-part2.pdf")
(code-pdftotext "grothams2" "$S/http/www.ams.org/notices/200410/fea-grothendieck-part2.pdf")
;; (find-grothams2page 1)
;; (find-grothams2text)
;; (find-grothams1page 1)
;; (find-grothams1text)

;; The Rising Sea: Grothendieck on simplicity and generality I
;; Colin McLarty - 24 May 2003
;; http://www.math.jussieu.fr/~leila/grothendieckcircle/mclarty1.pdf
(code-ps        "mclartyrisingsea" "$S/http/www.math.jussieu.fr/~leila/grothendieckcircle/mclarty1.pdf")
(code-pdftotext "mclartyrisingsea" "$S/http/www.math.jussieu.fr/~leila/grothendieckcircle/mclarty1.pdf")
;; (find-mclartyrisingseapage 1)
;; (find-mclartyrisingseatext)



;; «gurevich»  (to ".gurevich")
;; http://research.microsoft.com/~gurevich/annotated.html
;; Dershowitz/Gurevich: "A Natural Axiomatization of Computability and Proof of Church's Thesis"
;;   http://research.microsoft.com/~gurevich/Opera/188.pdf
(code-ps        "gurevchurch" "$S/http/research.microsoft.com/~gurevich/Opera/188.pdf")
(code-xpdf      "gurevchurch" "$S/http/research.microsoft.com/~gurevich/Opera/188.pdf")
(code-pdftotext "gurevchurch" "$S/http/research.microsoft.com/~gurevich/Opera/188.pdf")
;; (find-gurevchurchpage 1)
;; (find-gurevchurchpage (+ -298 321) "3. Abstract state machines.")
;; (find-gurevchurchtext)



;; «hatcher»  (to ".hatcher")
;; Algebraic Topology (Hatcher, 2002)
;; http://www.math.cornell.edu/~hatcher/AT/ATpage.html
;; http://www.math.cornell.edu/~hatcher/AT/typography.html
;; http://www.math.cornell.edu/~hatcher/AT/AT.pdf
;; http://en.wikipedia.org/wiki/Long_exact_sequence
;; http://en.wikipedia.org/wiki/Eilenberg-Steenrod_axioms
(code-ps        "hatcherat" "$S/http/www.math.cornell.edu/~hatcher/AT/AT.pdf")
(code-pdftotext "hatcherat" "$S/http/www.math.cornell.edu/~hatcher/AT/AT.pdf")
;; (find-hatcheratpage 1)
;; (find-hatcheratpage (+ 9 160))
;; (find-hatcherattext)


;; «henkin»  (to ".henkin")
;; Leon Henkin: "On Mathematical Induction"
;; http://www.jstor.org/stable/info/2308975
;; http://www.jstor.org/stable/pdfplus/2308975.pdf
(code-xpdf      "henkin60" "$S/http/www.jstor.org/stable/pdfplus/2308975.pdf")
(code-pdftotext "henkin60" "$S/http/www.jstor.org/stable/pdfplus/2308975.pdf")
;; (find-henkin60page 1)
;; (find-henkin60text)


;; «hoare»  (to ".hoare")
;; http://en.wikipedia.org/wiki/Communicating_Sequential_Processes
;; http://www.usingcsp.com/cspbook.pdf
(code-ps        "cspbook" "$S/http/www.usingcsp.com/cspbook.pdf")
(code-pdftotext "cspbook" "$S/http/www.usingcsp.com/cspbook.pdf")
;; (find-cspbookpage 1)
;; (find-cspbooktext)


;; «hodges»  (to ".hodges")
;; Wilfrid Hodges: "The mathematical core of Tarski's truth definition"
;; http://www.maths.qmul.ac.uk/~wilfrid/unilog07.pdf
(code-xpdf      "hodgestarski" "$S/http/www.maths.qmul.ac.uk/~wilfrid/unilog07.pdf")
(code-pdftotext "hodgestarski" "$S/http/www.maths.qmul.ac.uk/~wilfrid/unilog07.pdf")
;; (find-hodgestarskipage 1)
;; (find-hodgestarskitext)



;; «hofmann»  (to ".hofmann")
;; http://www.tcs.informatik.uni-muenchen.de/~mhofmann/papers.html
;; "Extensional concepts in intensional type theory" (thesis, 1995):
;;   http://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/ECS-LFCS-95-327.dvi
(code-dvi       "hofmannthesis" "$S/http/www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/ECS-LFCS-95-327.dvi")
(code-pdftotext "hofmannthesis" "$S/http/www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/ECS-LFCS-95-327.pdf")
;; (find-hofmannthesispage 1)
;; (find-hofmannthesistext)
;; (find-hofmannthesistext "definitional equality arises in category theory")
;; (find-hofmannthesistext "internalises proofs of equality")

;; "Semantical Analysis of higher-order abstract syntax":
;;   http://www.tcs.informatik.uni-muenchen.de/~mhofmann/lics99hoas.ps.gz
;; "Syntax and Semantics of Dependent Types":
;;   http://www.dcs.ed.ac.uk/home/mxh/cupart.dvi.gz
(code-dvi       "hofmann97ss" "$S/http/www.dcs.ed.ac.uk/home/mxh/cupart.dvi.gz")
(code-pdftotext "hofmann97ss" "$S/http/www.dcs.ed.ac.uk/home/mxh/cupart.pdf")
;; (find-hofmann97sspage 1)
;; (find-hofmann97sstext)


;; «jacobs»  (to ".jacobs")
;; http://www.cs.ru.nl/B.Jacobs/PAPERS/PhD.ps
(code-ps        "jacobsphd" "$S/http/www.cs.ru.nl/B.Jacobs/PAPERS/PhD.ps")
(code-pdftotext "jacobsphd" "$S/http/www.cs.ru.nl/B.Jacobs/PAPERS/PhD.ps")
;; (find-jacobsphdpage 1)
;; (find-jacobsphdpage 54 "CC-categories")
;; (find-jacobsphdpage 66 "References")
;; (find-jacobsphdtext)


;; «jibladze»  (to ".jibladze")
;; Mamuka Jibladze: "Almost Alexandroff topologies" (slides)
;; http://www.rmi.acnet.ge/tolo/presentations/JibladzeTbilisi2008beamer.pdf
(code-xpdf      "jibalextop" "$S/http/www.rmi.acnet.ge/tolo/presentations/JibladzeTbilisi2008beamer.pdf")
(code-pdftotext "jibalextop" "$S/http/www.rmi.acnet.ge/tolo/presentations/JibladzeTbilisi2008beamer.pdf")
;; (find-jibalextoppage 1)
;; (find-jibalextoptext)



;; «joao_marcos»  (to ".joao_marcos")
;; http://www.dimap.ufrn.br/~jmarcos/
;; http://www.math.ist.utl.pt/~jmarcos/Thesis/
;; http://wslc.math.ist.utl.pt/ftp/pub/MarcosJ/05-M-PhDthesis.pdf
(code-ps        "jmthesis" "$S/http/wslc.math.ist.utl.pt/ftp/pub/MarcosJ/05-M-PhDthesis.pdf")
(code-pdftotext "jmthesis" "$S/http/wslc.math.ist.utl.pt/ftp/pub/MarcosJ/05-M-PhDthesis.pdf")
;; (find-jmthesispage 1)
;; (find-jmthesispage 11)
;; (find-jmthesispage (+ 14 13) "The birth of paraconsistent logic")
;; (find-jmthesispage (+ 4 67)  "Appendix: Brief historical note")
;; (find-jmthesispage (+ 72 1)  "Chapter One")
;; (find-jmthesistext)
;; (find-jmthesistext "\n\nThe birth of paraconsistent logic")
;; (find-jmthesistext "\n\nAppendix: Brief historical note")
;; (find-jmthesistext "\fChapter One")



;; «johnstone»  (to ".johnstone")
(code-djvu "stonespaces" "~/books/johnstone_stone_spaces.djvu")
(code-djvu "topostheory" "~/books/johnstone_topos_theory.djvu")
(code-xpdf "elephantA"   "~/books/johnstone_elephant_A.pdf")
(code-xpdf "elephantBCD" "~/books/johnstone_elephant_BCD.pdf")
;; (find-stonespacespage 3 "Contents")
;; (find-stonespacespage (+ 20 169) "V. 1. A Crash Course in Sheaf Theory")
;; (find-stonespacespage (+ 20 368) "Index of Definitions")
;;
;; (find-topostheorypage 7 "Contents")
;; (find-topostheorypage (+ 24  90) "3.4. sh_j(E) as a Category of Fractions")
;; (find-topostheorypage (+ 24 319) "9.4. The Filter-Power Construction")
;; (find-topostheorypage (+ 24 347) "Bibliography")
;; (find-topostheorypage (+ 24 357) "Index of Definitions")
;; (find-topostheorypage (+ 24 361) "Index of Notation")
;;
;; (find-elephantApage     7 "Contents Volume 1")
;; (find-elephantApage     8 "Contents Volume 2")
;; (find-elephantBCDpage 854 "Bibliography")
;; (find-elephantBCDpage 881 "Index of Notation")
;; (find-elephantBCDpage 884 "General Index")
;; (find-elephantApage   (+/2 10 161) "A4 Geometric Morphisms - Basic Theory")
;; (find-elephantBCDpage (+ -234 471) "C1.1 Frames and Nuclei")

;; "Sites" (notes, 2005)
;;   http://www.math.ucl.ac.be/membres/topos/NotesJohnstone.pdf
(code-ps        "johnstonesites" "$S/http/www.math.ucl.ac.be/membres/topos/NotesJohnstone.pdf")
(code-pdftotext "johnstonesites" "$S/http/www.math.ucl.ac.be/membres/topos/NotesJohnstone.pdf")
;; (find-johnstonesitespage 1)
;; (find-johnstonesitestext)





;; «kanovei»  (to ".kanovei")
;; (to "nelson")
;; Kanovei: "IST is more than an algorithm to prove ZFC theorems" (1993)
;; http://arxiv.org/abs/math/9310213
;; http://arxiv.org/abs/math/9310213v1.pdf
(code-ps        "kanovei93" "$S/http/arxiv.org/abs/math/9310213v1.pdf")
(code-pdftotext "kanovei93" "$S/http/arxiv.org/abs/math/9310213v1.pdf")
;; (find-kanovei93page 1)
;; (find-kanovei93text)



;; «keisler»  (to ".keisler")
;; Jerome Keisler: "Elementary Calculus: An Approach Using Infinitesimals"
;; http://www.math.wisc.edu/~keisler/calc.html
;; http://www.math.wisc.edu/~keisler/chapter_1a.pdf





;; «kelly»  (to ".kelly")
;; Kelly: "Basic Concepts of Enriched Category Theory"
;; http://www.tac.mta.ca/tac/reprints/articles/10/tr10.dvi
;; http://www.tac.mta.ca/tac/reprints/articles/10/tr10.pdf
(code-dvi       "kellyenrich" "$S/http/www.tac.mta.ca/tac/reprints/articles/10/tr10.dvi")
(code-pdftotext "kellyenrich" "$S/http/www.tac.mta.ca/tac/reprints/articles/10/tr10.pdf")
;; (find-kellyenrichpage 1)
;; (find-kellyenrichtext)

;; Kelly/Lack: "On Property-Like Structures"
;; http://www.tac.mta.ca/tac/volumes/1997/n9/n9.dvi
;; http://www.tac.mta.ca/tac/volumes/1997/n9/n9.pdf
(code-dvi       "propstruct" "$S/http/www.tac.mta.ca/tac/volumes/1997/n9/n9.dvi")
(code-pdftotext "propstruct" "$S/http/www.tac.mta.ca/tac/volumes/1997/n9/n9.pdf")
;; (find-propstructpage (+ -212 240) "(i) T is property-like")
;; (find-propstructtext              "(i) T is property-like")
;; (find-propstructpage 1)
;; (find-propstructtext)



;; «kock»  (to ".kock")
;; Kock, Anders: A simple axiomatics for differentiation.
;; Math. Scand. 40 (1977), no. 2, 183-193.
;; http://www.mscand.dk/
;; http://www.mscand.dk/article.php?id=2356
;; http://www.mscand.dk/band_40_224073_3131.pdf
;; (find-sh0 "mv -v /tmp/band_40_224073_3131.pdf $S/http/www.mscand.dk/")
(code-ps   "kockdiff" "$S/http/www.mscand.dk/band_40_224073_3131.pdf")
(code-xpdf "kockdiff" "$S/http/www.mscand.dk/band_40_224073_3131.pdf")
;; (find-kockdiffpage 1)

;; Synthetic Differential Geometry (Second Edition):
;; http://home.imf.au.dk/kock/sdg99.pdf
(code-ps        "kocksdg" "$S/http/home.imf.au.dk/kock/sdg99.pdf")
(code-pdftotext "kocksdg" "$S/http/home.imf.au.dk/kock/sdg99.pdf")
;; (find-kocksdgpage 1)
;; (find-kocksdgtext)

;; Aspects of fractional exponent functors (Kock / Reyes)
;; http://www.tac.mta.ca/tac/volumes/1999/n10/5-10abs.html
;; http://www.tac.mta.ca/tac/volumes/1999/n10/n10.pdf
(code-ps        "kocktac99" "$S/http/www.tac.mta.ca/tac/volumes/1999/n10/n10.pdf")
(code-pdftotext "kocktac99" "$S/http/www.tac.mta.ca/tac/volumes/1999/n10/n10.pdf")
;; (find-kocktac99page 1)
;; (find-kocktac99text)

;; «kondratiev»  (to ".kondratiev")
;; G.V. Kondratiev: "Manifolds, Structures Categorically" (2006)
;; http://arxiv.org/abs/math/0608503
;; http://arxiv.org/abs/math/0608503v1.pdf
(code-ps        "manifscat" "$S/http/arxiv.org/abs/math/0608503v1.pdf")
(code-pdftotext "manifscat" "$S/http/arxiv.org/abs/math/0608503v1.pdf")
;; (find-manifscatpage 1)
;; (find-manifscattext)



;; «lamport»  (to ".lamport")
;; Leslie Lamport:
;; http://research.microsoft.com/users/lamport/pubs/pubs.html
;; "How to Write a Proof" (1993):
;;   http://research.microsoft.com/users/lamport/pubs/lamport-how-to-write.pdf
;; "How to Write a Long Formula" (1994):
;;   http://research.microsoft.com/users/lamport/pubs/lamport-howtowrite.pdf
;; "Substitution: Syntactic versus Semantic" (1998):
;;   http://research.microsoft.com/users/lamport/pubs/substitution.pdf
;; "Should Your Specification Language Be Typed?" (1997/1999, with Larry Paulson):
;;   http://research.microsoft.com/users/lamport/pubs/lamport-types.pdf
;;   http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-147.html
;;   http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-147.pdf
(code-ps        "lamportproofs" "$S/http/research.microsoft.com/users/lamport/pubs/lamport-how-to-write.pdf")
(code-pdftotext "lamportproofs" "$S/http/research.microsoft.com/users/lamport/pubs/lamport-how-to-write.pdf")
(code-ps        "lamportlongformula" "$S/http/research.microsoft.com/users/lamport/pubs/lamport-howtowrite.pdf")
(code-pdftotext "lamportlongformula" "$S/http/research.microsoft.com/users/lamport/pubs/lamport-howtowrite.pdf")
(code-ps        "lamportsubstitution" "$S/http/research.microsoft.com/users/lamport/pubs/substitution.pdf")
(code-pdftotext "lamportsubstitution" "$S/http/research.microsoft.com/users/lamport/pubs/substitution.pdf")
(code-ps        "lamporttypes" "$S/http/research.microsoft.com/users/lamport/pubs/lamport-types.pdf")
(code-pdftotext "lamporttypes" "$S/http/research.microsoft.com/users/lamport/pubs/lamport-types.pdf")
(code-ps        "lamporttypes2" "$S/http/www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-147.pdf")
(code-pdftotext "lamporttypes2" "$S/http/www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-147.pdf")
;; (find-lamportproofspage 1)
;; (find-lamportproofstext)
;; (find-lamportlongformulapage 1)
;; (find-lamportlongformulatext)
;; (find-lamportsubstitutionpage 1)
;; (find-lamportsubstitutiontext)
;; (find-lamporttypespage 1)
;; (find-lamporttypestext)
;; (find-lamporttypes2page 1)
;; (find-lamporttypes2text)




;; «lawvere»  (to ".lawvere")
;; http://www.tac.mta.ca/tac/reprints/
;; "Functorial Semantics of Algebraic Theories" (thesis, 1963):
;;   http://www.tac.mta.ca/tac/reprints/articles/5/tr5.dvi
;;   http://www.tac.mta.ca/tac/reprints/articles/5/tr5.pdf
;; "Adjointness in Foundations" (1969):
;;   http://www.tac.mta.ca/tac/reprints/articles/16/tr16.dvi
;;   http://www.tac.mta.ca/tac/reprints/articles/16/tr16.pdf
;; Lawvere: "Diagonal Arguments and Cartesian Closed Categories"
;;   http://www.tac.mta.ca/tac/reprints/articles/15/tr15.dvi
;;   http://www.tac.mta.ca/tac/reprints/articles/15/tr15.pdf
(code-dvi       "lawverethesis" "$S/http/www.tac.mta.ca/tac/reprints/articles/5/tr5.dvi")
(code-pdftotext "lawverethesis" "$S/http/www.tac.mta.ca/tac/reprints/articles/5/tr5.pdf")
(code-dvi       "lawvereadj" "$S/http/www.tac.mta.ca/tac/reprints/articles/16/tr16.dvi")
(code-pdftotext "lawvereadj" "$S/http/www.tac.mta.ca/tac/reprints/articles/16/tr16.pdf")
(code-dvi       "lawverediag" "$S/http/www.tac.mta.ca/tac/reprints/articles/15/tr15.dvi")
(code-pdftotext "lawverediag" "$S/http/www.tac.mta.ca/tac/reprints/articles/15/tr15.pdf")
;; (find-lawverethesispage 1)
;; (find-lawverethesistext)
;; (find-lawverethesistext "semantics has an adjoint called \"structure\"")
;; (find-lawvereadjpage 1)
;; (find-lawvereadjtext)
;; (find-lawvereadjpage 11 "A hyperdoctrine shall consist of")
;; (find-lawvereadjtext    "A hyperdoctrine shall consist of")
;; (find-lawverediagpage 1)
;; (find-lawverediagtext)

;; Peter Smith's notes on Galois Connections
;; http://logicmatters.blogspot.com/2008/05/galois-connections.html
;; http://www.phil.cam.ac.uk/teaching_staff/Smith/blogstuff/OrderGalois.pdf
(code-ps        "smithadj" "$S/http/www.phil.cam.ac.uk/teaching_staff/Smith/blogstuff/OrderGalois.pdf")
(code-pdftotext "smithadj" "$S/http/www.phil.cam.ac.uk/teaching_staff/Smith/blogstuff/OrderGalois.pdf")
;; (find-smithadjpage 20 "Syntax and semantics" "Adjointness in foundations")
;; (find-smithadjtext    "Syntax and semantics" "Adjointness in foundations")







;; «leinster»  (to ".leinster")
;; http://www.maths.gla.ac.uk/~tl/sheaves.pdf
(code-ps        "leinstersheaves" "$S/http/www.maths.gla.ac.uk/~tl/sheaves.pdf")
(code-pdftotext "leinstersheaves" "$S/http/www.maths.gla.ac.uk/~tl/sheaves.pdf")
;; (find-leinstersheavespage 1)
;; (find-leinstersheavestext)

;; «levy»  (to ".levy")
;; Paul Blain Levy: Adjunction models for call-by-push-value with stacks
;; http://www.tac.mta.ca/tac/volumes/14/5/14-05abs.html
;; http://www.tac.mta.ca/tac/volumes/14/5/14-05.dvi
(code-dvi "cbpv" "$S/http/www.tac.mta.ca/tac/volumes/14/5/14-05.dvi")
;; (find-cbpvpage (+ -74 75))

;; Paul Blain Levy: Typed Lambda Calculus
;; http://www.cs.bham.ac.uk/~pbl/mgs/lam/index.html
;; http://www.cs.bham.ac.uk/~pbl/mgs/lam/mgsbegin.pdf
;; http://www.cs.bham.ac.uk/~pbl/mgs/lam/mgscontinue.pdf
;; http://www.cs.bham.ac.uk/~pbl/mgs/lam/mgsdiverge.pdf
;; http://www.cs.bham.ac.uk/~pbl/mgs/lam/mgscbv.pdf
;; http://www.cs.bham.ac.uk/~pbl/mgs/lam/mgsanswers.pdf
(code-ps        "pbltlc1" "$S/http/www.cs.bham.ac.uk/~pbl/mgs/lam/mgsbegin.pdf")
(code-pdftotext "pbltlc1" "$S/http/www.cs.bham.ac.uk/~pbl/mgs/lam/mgsbegin.pdf")
(code-ps        "pbltlc2" "$S/http/www.cs.bham.ac.uk/~pbl/mgs/lam/mgscontinue.pdf")
(code-pdftotext "pbltlc2" "$S/http/www.cs.bham.ac.uk/~pbl/mgs/lam/mgscontinue.pdf")
(code-ps        "pbltlc3" "$S/http/www.cs.bham.ac.uk/~pbl/mgs/lam/mgsdiverge.pdf")
(code-pdftotext "pbltlc3" "$S/http/www.cs.bham.ac.uk/~pbl/mgs/lam/mgsdiverge.pdf")
(code-ps        "pbltlc4" "$S/http/www.cs.bham.ac.uk/~pbl/mgs/lam/mgscbv.pdf")
(code-pdftotext "pbltlc4" "$S/http/www.cs.bham.ac.uk/~pbl/mgs/lam/mgscbv.pdf")
(code-ps        "pbltlc5" "$S/http/www.cs.bham.ac.uk/~pbl/mgs/lam/mgsanswers.pdf")
(code-pdftotext "pbltlc5" "$S/http/www.cs.bham.ac.uk/~pbl/mgs/lam/mgsanswers.pdf")
;; (find-pbltlc1page 1)
;; (find-pbltlc1text)
;; (find-pbltlc2page 1)
;; (find-pbltlc2text)
;; (find-pbltlc3page 1)
;; (find-pbltlc3text)
;; (find-pbltlc4page 1)
;; (find-pbltlc4text)
;; (find-pbltlc5page 1)
;; (find-pbltlc5text)

;; «luo»  (to ".luo")
;; http://www.cs.rhul.ac.uk/~zhaohui/books.html
;; http://www.cs.rhul.ac.uk/~zhaohui/THESIS90.ps.gz
;; http://www.cs.rhul.ac.uk/~zhaohui/THESIS90.dvi.gz
;; (find-sh0 "cd $S/http/www.cs.rhul.ac.uk/~zhaohui/ && zcat THESIS90.dvi.gz > THESIS90.dvi")
;; (find-sh0 "cd $S/http/www.cs.rhul.ac.uk/~zhaohui/ && dvipdf THESIS90.dvi")
(code-dvi       "luothesis" "$S/http/www.cs.rhul.ac.uk/~zhaohui/THESIS90.dvi.gz")
(code-pdftotext "luothesis" "$S/http/www.cs.rhul.ac.uk/~zhaohui/THESIS90.pdf")
;; (find-luothesispage 1)
;; (find-luothesistext)
;; (find-luothesistext          "The inference rules of ECC ")
;; (find-luothesispage (+ 6 16) "The inference rules of ECC ")
;; (find-luothesistext          "Definition 6.1.4 (Leibniz's equality)")
;; (find-luothesispage (+ 6 82) "Definition 6.1.4 (Leibniz's equality)")
;; (find-luothesistext           "Theorem 9.1.1 (equality reflection)")
;; (find-luothesispage (+ 6 110) "Theorem 9.1.1 (equality reflection)")





(code-ps "dout" "~/TESE/puc.pdf")
;; (find-doutpage 1)
;; (find-doutpage (+ 1 48))
;; (find-doutfile "dnc.metatex" "categoria de display")

;; A New Approach to Teaching Discrete Mathematics (Gries / Schneider, 2001)
;; http://www.cs.cornell.edu/fbs/fullist.htm
;; http://www.cs.cornell.edu/fbs/publications/GSprimus.ps
(code-ps       "griesschn" "$S/http/www.cs.cornell.edu/fbs/publications/GSprimus.ps")
(code-pstotext "griesschn" "$S/http/www.cs.cornell.edu/fbs/publications/GSprimus.ps")
;; (find-griesschnpage 1)
;; (find-griesschntext)

;; http://www.ru.is/luca/
;; http://www.cs.auc.dk/~luca/SV/intro2ccs.pdf
;; (find-reactsyspage)
(code-ps "reactsys" "$S/http/www.cs.auc.dk/~luca/SV/intro2ccs.pdf")


;; «martin-lof»  (to ".martin-lof")
;; Per Martin-Löf: On the Meanings of the Logical Constants and the
;; Justifications of the Logical Laws
;; http://www.hf.uio.no/ifikk/filosofi/njpl/vol1no1/meaning/meaning.dvi
;; http://www.hf.uio.no/ifikk/filosofi/njpl/vol1no1/meaning/meaning.pdf
(code-dvi       "mlcjll" "$S/http/www.hf.uio.no/ifikk/filosofi/njpl/vol1no1/meaning/meaning.dvi")
(code-pdftotext "mlcjll" "$S/http/www.hf.uio.no/ifikk/filosofi/njpl/vol1no1/meaning/meaning.pdf")
;; (find-mlcjllpage 1)
;; (find-mlcjlltext)



;; «mckinsey»  (to ".mckinsey")
;; McKinsey: "Solution of the Decision Problem for the Lewis Systems S2
;;   and S4 with an Application to Topology" (1941)
;; McKinsey/Tarski, A.: "The Algebra of Topology" (1944)
;; mckinsey41: http://www.jstor.org/stable/info/2267105
;; mckinsey44: http://www.jstor.org/stable/info/1969080
;; http://www.dimap.ufrn.br/~jmarcos/papers/S2nS4-McKinsey.pdf
;; http://www.dimap.ufrn.br/~jmarcos/papers/AoT-McKinsey_Tarski.pdf
(code-xpdf "mckinsey41" "$S/http/www.dimap.ufrn.br/~jmarcos/papers/S2nS4-McKinsey.pdf")
(code-xpdf "mckinsey44" "$S/http/www.dimap.ufrn.br/~jmarcos/papers/AoT-McKinsey_Tarski.pdf")
;; (find-mckinsey41page 1)
;; (find-mckinsey44page 1)


;; «moerdijk»  (to ".moerdijk")
;; Moerdijk/Reyes: "Models for Smooth Infinitesimal Analysis" (book)
(code-djvu "moerey" "~/books/moerdijk_reyes_models_for_sia.djvu")
;; (find-moereypage 8 "Contents")
;; (find-moereypage (+ 9  24) "I.2. Manifolds as Cinfty-rings")
;; (find-moereypage (+ 9 387) "Index")



;; «moggi»  (to ".moggi")
;; http://www.disi.unige.it/person/MoggiE/ftp/filter2.pdf
;; http://www.disi.unige.it/person/MoggiE/ftp/lics89.pdf
;; http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf
;; http://www.disi.unige.it/person/MoggiE/ftp/EM-GDPfest.pdf
(code-ps        "moggifilter" "$S/http/www.disi.unige.it/person/MoggiE/ftp/filter2.pdf")
(code-pdftotext "moggifilter" "$S/http/www.disi.unige.it/person/MoggiE/ftp/filter2.pdf")
(code-ps        "moggiclcm" "$S/http/www.disi.unige.it/person/MoggiE/ftp/lics89.pdf")

(code-pdftotext "moggiclcm" "$S/http/www.disi.unige.it/person/MoggiE/ftp/lics89.pdf")
(code-ps        "moggincm" "$S/http/www.disi.unige.it/person/MoggiE/ftp/ic91.pdf")
(code-pdftotext "moggincm" "$S/http/www.disi.unige.it/person/MoggiE/ftp/ic91.pdf")
(code-ps        "moggiplosymp" "$S/http/www.disi.unige.it/person/MoggiE/ftp/EM-GDPfest.pdf")
(code-pdftotext "moggiplosymp" "$S/http/www.disi.unige.it/person/MoggiE/ftp/EM-GDPfest.pdf")
;; (find-moggifilterpage 1)
;; (find-moggifiltertext)
;; (find-moggiclcmpage 1)
;; (find-moggiclcmtext)
;; (find-moggincmpage 1)
;; (find-moggincmtext)
;; (find-moggiplosymppage 1)
;; (find-moggiplosymptext)



;; «nelson»  (to ".nelson")
;; (to "kanovei")
;; http://www.math.princeton.edu/~nelson/
;; http://www.math.princeton.edu/~nelson/books/1.pdf
;; http://www.math.princeton.edu/~nelson/nelsonbib.pdf
;; http://www.math.princeton.edu/~nelson/papers/fog.pdf
(code-ps        "nelson1" "$S/http/www.math.princeton.edu/~nelson/books/1.pdf")
(code-pdftotext "nelson1" "$S/http/www.math.princeton.edu/~nelson/books/1.pdf")
(code-ps        "nelsonbib" "$S/http/www.math.princeton.edu/~nelson/nelsonbib.pdf")
(code-pdftotext "nelsonbib" "$S/http/www.math.princeton.edu/~nelson/nelsonbib.pdf")
(code-ps        "gnomesinthefog" "$S/http/www.math.princeton.edu/~nelson/papers/fog.pdf")
(code-pdftotext "gnomesinthefog" "$S/http/www.math.princeton.edu/~nelson/papers/fog.pdf")
;; (find-nelson1page 1)
;; (find-nelson1text)
;; (find-nelson1text "CHAPTER 1" "Internal Set Theory")
;; (find-nelsonbibpage 1)
;; (find-nelsonbibtext)
;; (find-nelsonbibtext "The syntax of nonstandard analysis")
;; (find-gnomesinthefogpage 1)
;; (find-gnomesinthefogtext)
;; (find-gnomesinthefogtext "but rather provided an extension")

(code-xpdf "nelson77" "~/tmp/Nelson_-_Internal_Set_Theory.pdf")
;; (find-nelson77page 1)
;; (find-nelson77page (+ -1164 1165))
;; (find-nelson77page (+ -1164 1192) "conservation theorem")


;; «palmgren»  (to ".palmgren")
;; Erik Palmgren: "Developments in Constructive Nonstandard Analysis"
;; http://www.jstor.org/stable/info/421031
;; http://www.jstor.org/stable/pdfplus/421031.pdf
(code-xpdf      "palmgrendicna" "$S/http/www.jstor.org/stable/pdfplus/421031.pdf")
(code-pdftotext "palmgrendicna" "$S/http/www.jstor.org/stable/pdfplus/421031.pdf")
;; (find-palmgrendicnapage 1)
;; (find-palmgrendicnatext)

;; http://citeseer.ist.psu.edu/palmgren99remark.html
;; (find-fline "~/tmp/palmgren99remark.pdf")
(code-ps        "palmgrenfilter" "~/tmp/palmgren99remark.pdf")
(code-ps        "palmgrenfilter" "~/tmp/palmgren99remark.ps.gz")
(code-pdftotext "palmgrenfilter" "~/tmp/palmgren99remark.pdf")
;; (find-palmgrenfilterpage 1)
;; (find-palmgrenfiltertext)



;; «pastro»  (to ".pastro")
;; http://www.maths.mq.edu.au/~craig/pdf/msc.pdf
(code-ps        "pastromsc" "$S/http/www.maths.mq.edu.au/~craig/pdf/msc.pdf")
(code-pdftotext "pastromsc" "$S/http/www.maths.mq.edu.au/~craig/pdf/msc.pdf")
;; (find-pastromscpage 1)
;; (find-pastromsctext)


;; «phoa»  (to ".phoa")
;; Wesley Phoa: "An introduction to fibrations, topos theory, the effective topos and modest sets"
;; http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/index.html
;; http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/ECS-LFCS-92-208.ps.gz
;; (find-sh "cd $S/http/www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/ && zcat ECS-LFCS-92-208.ps.gz | ps2pdf - ECS-LFCS-92-208.pdf")
(code-ps        "phoa" "$S/http/www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/ECS-LFCS-92-208.ps.gz")
(code-pdftotext "phoa" "$S/http/www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/ECS-LFCS-92-208.pdf")
;; (find-phoapage 1)
;; (find-phoapage 10 "fibred CCC")
;; (find-phoapage 17 "Beck-Chevalley condition")
;; (find-phoapage 18 "quantification commutes with substitution")
;; (find-phoapage 27 "comprehension categories")
;; (find-phoapage 55 "doctrinal diagram")
;; (find-phoapage 56 "Beck-Chevalley condition for quantifiers")
;; (find-phoapage 60 "Osius" "restricted modus ponens")
;; (find-phoapage 61 "the x such that")
;; (find-phoapage 68 "Extending the language")
;; (find-phoapage 131 "A version of constructive set theory")
;; (find-phoatext)


;; «pitts»  (to ".pitts")
;; Andrew Pitts:
;; http://www.cl.cam.ac.uk/~amp12/
;; Pitts: "Polymorphism is Set-Theoretic, Constructively":
;;   http://www.cl.cam.ac.uk/~amp12/papers/polist/polist.pdf
;; "Notes on Categorical Logic" (1989/1991):
;;   http://www.cl.cam.ac.uk/~amp12/papers/notcl/notcl.pdf
;; "Lecture Notes on Types" (1997-2007):
;;   http://www.cl.cam.ac.uk/teaching/0708/Types/typ.pdf
(code-xpdf      "pistc" "$S/http/www.cl.cam.ac.uk/~amp12/papers/polist/polist.pdf")
(code-xpdf      "pittsnocl" "$S/http/www.cl.cam.ac.uk/~amp12/papers/notcl/notcl.pdf")
(code-ps        "pittslntypes" "$S/http/www.cl.cam.ac.uk/teaching/0708/Types/typ.pdf")
(code-pdftotext "pittslntypes" "$S/http/www.cl.cam.ac.uk/teaching/0708/Types/typ.pdf")
;; (find-pistcpage 1)
;; (find-pittsnoclpage 1)
;; (find-pittslntypespage 1)
;; (find-pittslntypestext)





;; «reynolds»  (to ".reynolds")
;; Reynolds 1984: "Polymorphism is not Set-Theoretic"
;; LNCS version:
;;   http://www.informatik.uni-trier.de/~ley/db/conf/sdt/sdt1984.html
;;   http://dblp.uni-trier.de/rec/bibtex/conf/sdt/Reynolds84
;; Antiopolis version:
;;   http://www.inria.fr/rrrt/rr-0296.html
;;   ftp://ftp.inria.fr/INRIA/publication/publi-pdf/RR/RR-0296.pdf
(code-xpdf "pinst" "$S/ftp/ftp.inria.fr/INRIA/publication/publi-pdf/RR/RR-0296.pdf")
;; (find-pinstpage 1)



;; «rosolini»  (to ".rosolini")
;; Giuseppe Rosolini:
;; http://www.disi.unige.it/person/RosoliniG/biblio.html
;; "Continuity and Effectiveness in Topoi":
;;   ftp://ftp.disi.unige.it/pub/person/RosoliniG/papers/coneit.ps.gz
;; Freyd/Robinson/Rosolini: "Dinaturality for free"
;;   ftp://ftp.disi.unige.it/pub/person/RosoliniG/papers/dinff.ps.gz
;; "About Modest Sets":
;;   ftp://ftp.disi.unige.it/pub/person/RosoliniG/papers/aboms.ps.gz
;; (find-sh "cd $S/ftp/ftp.disi.unige.it/pub/person/RosoliniG/papers/ && zcat coneit.ps.gz | ps2pdf - coneit.pdf")
;; (find-sh "cd $S/ftp/ftp.disi.unige.it/pub/person/RosoliniG/papers/ && zcat dinff.ps.gz | ps2pdf - dinff.pdf")
;; (find-sh "cd $S/ftp/ftp.disi.unige.it/pub/person/RosoliniG/papers/ && zcat aboms.ps.gz | ps2pdf - aboms.pdf")
(code-ps        "coneit" "$S/ftp/ftp.disi.unige.it/pub/person/RosoliniG/papers/coneit.ps.gz")
(code-pdftotext "coneit" "$S/ftp/ftp.disi.unige.it/pub/person/RosoliniG/papers/coneit.pdf")
(code-ps        "dinff"  "$S/ftp/ftp.disi.unige.it/pub/person/RosoliniG/papers/dinff.ps.gz")
(code-pdftotext "dinff"  "$S/ftp/ftp.disi.unige.it/pub/person/RosoliniG/papers/dinff.pdf")
(code-ps        "aboms"  "$S/ftp/ftp.disi.unige.it/pub/person/RosoliniG/papers/aboms.ps.gz")
(code-pdftotext "aboms"  "$S/ftp/ftp.disi.unige.it/pub/person/RosoliniG/papers/aboms.pdf")
;; (find-abomspage 1)
;; (find-abomstext)
;; (find-dinffpage 1)
;; (find-dinfftext)
;; (find-coneitpage 0)
;; (find-coneittext)



;; «schalk»  (to ".schalk")
;; Andrea Schalk's notes:
;; http://www.cs.man.ac.uk/~schalk/notes/
;; http://www.cs.man.ac.uk/~schalk/notes/intgam.ps.gz
;; http://www.cs.man.ac.uk/~schalk/notes/llmodel.ps.gz
;; http://www.cs.man.ac.uk/~schalk/notes/monads.ps.gz
;; http://www.cs.man.ac.uk/~schalk/publ/gomll.ps.gz
(code-ps "schalkintgam"  "$S/http/www.cs.man.ac.uk/~schalk/notes/intgam.ps.gz")
(code-ps "schalkllmodel" "$S/http/www.cs.man.ac.uk/~schalk/notes/llmodel.ps.gz")
(code-ps "schalkmonads"  "$S/http/www.cs.man.ac.uk/~schalk/notes/monads.ps.gz")
(code-ps "schalkortog"   "$S/http/www.cs.man.ac.uk/~schalk/publ/gomll.ps.gz")
;; (find-schalkintgampage 1)
;; (find-schalkllmodelpage 1)
;; (find-schalkmonadspage 1)
;; (find-schalkortogpage 1)



;; «seely»  (to ".seely")

;; Seely:
;; http://www.math.mcgill.ca/rags/
;; http://www.math.mcgill.ca/rags/linear/lfl.ps.gz
;; http://www.math.mcgill.ca/rags/bang/bang.ps.gz
;; http://www.math.mcgill.ca/rags/linear/wdc.ps.gz
;; http://www.math.mcgill.ca/rags/nets/nets.ps.gz
;; http://www.math.mcgill.ca/rags/nets/llsac.ps.gz
;; http://www.math.mcgill.ca/rags/bicats/bicat.ps.gz
(code-ps "ragsstorage" "$S/http/www.math.mcgill.ca/rags/bang/bang.ps.gz")
(code-ps "ragslinearf" "$S/http/www.math.mcgill.ca/rags/linear/lfl.ps.gz")
(code-ps "ragsnets"    "$S/http/www.math.mcgill.ca/rags/nets/nets.ps.gz")
(code-ps "ragswdc"     "$S/http/www.math.mcgill.ca/rags/linear/wdc.ps.gz")
(code-ps "rags89"      "$S/http/www.math.mcgill.ca/rags/nets/llsac.ps.gz")
(code-ps "ragsbicat"   "$S/http/www.math.mcgill.ca/rags/bicats/bicat.ps.gz")
;; (find-ragsstoragepage 1)
;; storage rules:                (find-ragsstoragepage 11)
;; strong and costrong functors: (find-ragsstoragepage 15)
;; (find-ragslinearfpage 1)
;; (find-ragswdcpage 1)
;; (find-ragsnetspage 1)
;; (find-rags89page 1)
;; (find-ragsbicatpage 1)

;; http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf
;; http://www.math.mcgill.ca/rags/ZML/ZML.PDF
(code-xpdf "ragslccc" "$S/http/www.math.mcgill.ca/rags/LCCC/LCCC.pdf")
(code-xpdf "ragshyp"  "$S/http/www.math.mcgill.ca/rags/ZML/ZML.PDF")
;; (find-ragslcccpage 1)
;; (find-ragshyppage 1)
;; (find-ragshyppage 7 "Beck condition")
;; (find-ragshyppage (+ -504 513))

;; Categorical Semantics for Higher Order Polymorphic Lambda Calculus (1987)
;; http://www.math.mcgill.ca/rags/JSL/PLC.pdf
(code-xpdf "ragsplc" "$S/http/www.math.mcgill.ca/rags/JSL/PLC.pdf")
;; (find-ragsplcpage 1)

;; Fock Space: A Model of Linear Exponential Types
;; (Blute / Panangaden / Seely)
;;    http://www.math.mcgill.ca/rags/fock/fock.ps.gz
;; -> http://www.math.mcgill.ca/rags/fock/fock.pdf
;; (find-sh "cd $S/http/www.math.mcgill.ca/rags/fock/ && zcat fock.ps.gz | ps2pdf - fock.pdf")
(code-ps        "seelyfock" "$S/http/www.math.mcgill.ca/rags/fock/fock.ps.gz")
(code-pdftotext "seelyfock" "$S/http/www.math.mcgill.ca/rags/fock/fock.pdf")
;; (find-seelyfockpage 1)
;; (find-seelyfocktext)

;; Differential categories (Blute / Cockett / Seely, 2005):
;; http://www.math.mcgill.ca/rags/difftl/difftl.ps.gz
;; http://www.math.mcgill.ca/rags/difftl/difftl.pdf   <--\
;; (find-sh "cd $S/http/www.math.mcgill.ca/rags/difftl/ && zcat difftl.ps.gz | ps2pdf - difftl.pdf")
(code-ps        "ragsdiff" "$S/http/www.math.mcgill.ca/rags/difftl/difftl.ps.gz")
(code-pdftotext "ragsdiff" "$S/http/www.math.mcgill.ca/rags/difftl/difftl.pdf")
;; (find-ragsdiffpage 1)
;; (find-ragsdifftext)

;; Slides (about Differential Categories):
;; http://www.math.mcgill.ca/rags/difftl/DiffCats_Seely-CMS-June06.pdf
;; http://www.math.mcgill.ca/rags/difftl/DiffCats2_Seely-CT06-June06.pdf
;; http://www.math.mcgill.ca/rags/difftl/DiffCats3_Seely-CT07-June07.pdf
(code-ps "ragsdiff1" "$S/http/www.math.mcgill.ca/rags/difftl/DiffCats_Seely-CMS-June06.pdf")
(code-ps "ragsdiff2" "$S/http/www.math.mcgill.ca/rags/difftl/DiffCats2_Seely-CT06-June06.pdf")
(code-ps "ragsdiff3" "$S/http/www.math.mcgill.ca/rags/difftl/DiffCats3_Seely-CT07-June07.pdf")
;; (find-ragsdiff1page 1)
;; (find-ragsdiff2page 1)
;; (find-ragsdiff3page 19)

;; Polarized Category Theory, Modules, and Game Semantics
;; (Cockett / Seely, 2007)
;; http://www.math.mcgill.ca/rags/games/games.ps.gz
(code-ps "ragsgames" "$S/http/www.math.mcgill.ca/rags/games/games.ps.gz")
;; (find-ragsgamespage 1)
;; Related: Craig Pastro's thesis
;;  (find-pastromscpage 1)



;; «shulman»  (to ".shulman")
;; Shulman: "Set Theory for Category Theory"
;; http://www.math.uchicago.edu/~shulman/exposition/
;; http://arxiv.org/abs/0810.1279
;; http://arxiv.org/abs/0810.1279v2.dvi
;; http://arxiv.org/abs/0810.1279v2.pdf
;; (find-fline "$S/http/arxiv.org/abs/" "0810.1279")
;; (find-sh0 "mv -iv /tmp/0810.1279* $S/http/arxiv.org/abs/")
(code-dvi       "stforct" "$S/http/arxiv.org/abs/0810.1279v2.dvi")
(code-xpdf      "stforct" "$S/http/arxiv.org/abs/0810.1279v2.pdf")
(code-pdftotext "stforct" "$S/http/arxiv.org/abs/0810.1279v2.pdf")
;; (find-stforctpage 1)
;; (find-stforcttext)



;; «simmons»  (to ".simmons")
;; Harold Simmons' notes:
;; http://www.cs.man.ac.uk/~hsimmons/DOCUMENTS/papersandnotes.html
;; http://www.cs.man.ac.uk/~hsimmons/DOCUMENTS/PAPERSandNOTES/Omegasets.ps.gz
;; (find-sh "cd $S/http/www.cs.man.ac.uk/~hsimmons/DOCUMENTS/PAPERSandNOTES/ && zcat Omegasets.ps.gz | ps2pdf - Omegasets.pdf")
(code-ps       "simmonspsh" "$S/http/www.cs.man.ac.uk/~hsimmons/DOCUMENTS/PAPERSandNOTES/Omegasets.ps.gz")
(code-ps        "omegasets" "$S/http/www.cs.man.ac.uk/~hsimmons/DOCUMENTS/PAPERSandNOTES/Omegasets.ps.gz")
(code-pdftotext "omegasets" "$S/http/www.cs.man.ac.uk/~hsimmons/DOCUMENTS/PAPERSandNOTES/Omegasets.pdf")
;; (find-omegasetspage 1)
;; (find-omegasetstext)

;; http://www.cs.man.ac.uk/~hsimmons/FRAMES/frames.html
;; http://www.cs.man.ac.uk/~hsimmons/MAGIC-CATS/magic-cats.html
;; http://www.cs.man.ac.uk/~hsimmons/FRAMES/Z-Overview.pdf
;; http://www.cs.man.ac.uk/~hsimmons/FRAMES/A-Basics.pdf
;; http://www.cs.man.ac.uk/~hsimmons/FRAMES/B-Assembly.pdf
;; http://www.cs.man.ac.uk/~hsimmons/FRAMES/C-POINTSPACE.pdf
;; http://www.cs.man.ac.uk/~hsimmons/FRAMES/D-FUNDTRIANGLE.pdf
(code-ps        "simmonsfrZ" "$S/http/www.cs.man.ac.uk/~hsimmons/FRAMES/Z-Overview.pdf")
(code-pdftotext "simmonsfrZ" "$S/http/www.cs.man.ac.uk/~hsimmons/FRAMES/Z-Overview.pdf")
(code-ps        "simmonsfrA" "$S/http/www.cs.man.ac.uk/~hsimmons/FRAMES/A-Basics.pdf")
(code-pdftotext "simmonsfrA" "$S/http/www.cs.man.ac.uk/~hsimmons/FRAMES/A-Basics.pdf")
(code-ps        "simmonsfrB" "$S/http/www.cs.man.ac.uk/~hsimmons/FRAMES/B-Assembly.pdf")
(code-pdftotext "simmonsfrB" "$S/http/www.cs.man.ac.uk/~hsimmons/FRAMES/B-Assembly.pdf")
(code-ps        "simmonsfrC" "$S/http/www.cs.man.ac.uk/~hsimmons/FRAMES/C-POINTSPACE.pdf")
(code-pdftotext "simmonsfrC" "$S/http/www.cs.man.ac.uk/~hsimmons/FRAMES/C-POINTSPACE.pdf")
(code-ps        "simmonsfrD" "$S/http/www.cs.man.ac.uk/~hsimmons/FRAMES/D-FUNDTRIANGLE.pdf")
(code-pdftotext "simmonsfrD" "$S/http/www.cs.man.ac.uk/~hsimmons/FRAMES/D-FUNDTRIANGLE.pdf")
;; (find-simmonsfrZpage 1)
;; (find-simmonsfrZtext)
;; (find-simmonsfrApage 1)
;; (find-simmonsfrAtext)
;; (find-simmonsfrBpage 1)
;; (find-simmonsfrBtext)
;; (find-simmonsfrCpage 1)
;; (find-simmonsfrCpage 2 "The point space construction")
;; (find-simmonsfrCtext)
;; (find-simmonsfrDpage 1)
;; (find-simmonsfrDtext)



;; «simpson»  (to ".simpson")
;; Alex Simpson: "The Proof Theory and Semantics of Intuitionistic Modal Logic"
;; http://homepages.inf.ed.ac.uk/als/Research/thesis.ps.gz
;; (find-sh "cd $S/http/homepages.inf.ed.ac.uk/als/Research/ && zcat thesis.ps.gz | ps2pdf - thesis.pdf")
(code-ps        "simpsonthesis" "$S/http/homepages.inf.ed.ac.uk/als/Research/thesis.ps.gz")
(code-pdftotext "simpsonthesis" "$S/http/homepages.inf.ed.ac.uk/als/Research/thesis.pdf")
;; (find-simpsonthesispage 1)
;; (find-simpsonthesistext)



;; «street»  (to ".street")
;; Ross Street: "Monoidal categories for the combinatorics of group representations"
;; http://www.math.mq.edu.au/~street/Droup.pdf
;; (find-sh "cd $S/http/www.math.mq.edu.au/~street/ && zcat Droup.pdf | ps2pdf - Droup.pdf.pdf")
(code-ps        "droup" "$S/http/www.math.mq.edu.au/~street/Droup.pdf")
(code-pdftotext "droup" "$S/http/www.math.mq.edu.au/~street/Droup.pdf")
;; (find-drouppage 1)
;; (find-drouptext)



;; «streicher»  (to ".streicher")
;; http://www.mathematik.tu-darmstadt.de/~streicher/

;; "Fibred Categories à la Jean Bénabou":
;; http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/FibLec.pdf.gz
;; http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/FibLec.pdf
;; (find-sh "cd $S/http/www.mathematik.tu-darmstadt.de/~streicher/FIBR/ && gunzip FibLec.pdf.gz")
(code-ps        "streicherbenabou" "$S/http/www.mathematik.tu-darmstadt.de/~streicher/FIBR/FibLec.pdf")
(code-pdftotext "streicherbenabou" "$S/http/www.mathematik.tu-darmstadt.de/~streicher/FIBR/FibLec.pdf")
;; (find-streicherbenaboupage 1)
;; (find-streicherbenaboutext)

;; Peter Lietz's MsC thesis
;; http://www.mathematik.tu-darmstadt.de/~streicher/
;; http://www.mathematik.tu-darmstadt.de/~streicher/index.html
;; http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/lietz.ps.gz
;; (find-sh "cd $S/http/www.mathematik.tu-darmstadt.de/~streicher/FIBR/ && zcat lietz.ps.gz | ps2pdf - lietz.pdf")
(code-ps        "lietzfibr" "$S/http/www.mathematik.tu-darmstadt.de/~streicher/FIBR/lietz.ps.gz")
(code-pdftotext "lietzfibr" "$S/http/www.mathematik.tu-darmstadt.de/~streicher/FIBR/lietz.pdf")
;; (find-lietzfibrpage 1)
;; (find-lietzfibrpage 4)
;; (find-lietzfibrtext)

;; Thomas Streicher's PhD thesis: "Investigations Into Intensional Type Theory"
;; http://www.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf
(code-xpdf      "streicherthesis" "$S/http/www.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf")
(code-pdftotext "streicherthesis" "$S/http/www.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf")
;; (find-streicherthesispage 1)
;; (find-streicherthesispage 9 "refute propositions which suspected to be underivable")
;; (find-streicherthesispage 16 "Luo")
;; (find-streicherthesistext)




;; «taylor»  (to ".taylor")
;; Paul Taylor's thesis: "Recursive Domains, Indexed Category Theory and Polymorphism"
;; http://www.monad.me.uk/domains/
;; http://www.monad.me.uk/domains/recdic.dvi
;; (find-sh "cd $S/http/www.monad.me.uk/domains/ && dvipdf recdic.dvi")
(code-dvi       "paultaylorthesis" "$S/http/www.monad.me.uk/domains/recdic.dvi")
(code-pdftotext "paultaylorthesis" "$S/http/www.monad.me.uk/domains/recdic.pdf")
;; (find-paultaylorthesispage 1)
;; (find-paultaylorthesispage (+ 11  75) "role of variables")
;; (find-paultaylorthesispage (+ 11  97) "(rules)")
;; (find-paultaylorthesispage (+ 11 101) "Indexed categories")
;; (find-paultaylorthesispage (+ 11 132) "Pullback may destroy top or bounded completeness")
;; (find-paultaylorthesistext)

;; Paul Taylor: "Towards a Unified Treatment of Induction (Abstract)" (1996)
;; http://www.monad.me.uk/ordinals/towuti-abs.dvi
;; http://www.monad.me.uk/ordinals/towuti-abs.pdf
(code-dvi       "towutiabs" "$S/http/www.monad.me.uk/ordinals/towuti-abs.dvi")
(code-pdftotext "towutiabs" "$S/http/www.monad.me.uk/ordinals/towuti-abs.pdf")
;; (find-towutiabspage 1)
;; (find-towutiabstext)

;; Paul Taylor's notes for the Cambridge Tripos (scanned)
;; http://www.monad.me.uk/tripos/
;; http://www.monad.me.uk/tripos/Algebra-I-Groups.pdf
;; http://www.monad.me.uk/tripos/Algebra-2-Vector-Spaces.pdf
;; http://www.monad.me.uk/tripos/Algebra-Exercises.pdf
;; http://www.monad.me.uk/tripos/Electrodynamics.pdf
;; http://www.monad.me.uk/tripos/Linear-Systems.pdf
;; http://www.monad.me.uk/tripos/Probability.pdf
;; http://www.monad.me.uk/tripos/Gauss-Proof.pdf
;; http://www.monad.me.uk/tripos/Algebra-3.pdf
;; http://www.monad.me.uk/tripos/Complex-Variable.pdf
;; http://www.monad.me.uk/tripos/Rings+Modules.pdf
;; http://www.monad.me.uk/tripos/Galois.pdf
;; http://www.monad.me.uk/tripos/Representation.pdf
;; http://www.monad.me.uk/tripos/Groups.pdf

;; Paul Taylor: A Lambda Calculus for Real Analysis
;; http://www.monad.me.uk/slides/
;; http://www.monad.me.uk/ASD/analysis.php
;; http://www.monad.me.uk/ASD/lamcra.dvi
;; http://www.cs.man.ac.uk/~pt/ASD/lamcra.pdf
(code-ps        "lamcra" "$S/http/www.cs.man.ac.uk/~pt/ASD/lamcra.pdf")
(code-dvi       "lamcra" "$S/http/www.monad.me.uk/ASD/lamcra.dvi")
(code-pdftotext "lamcra" "$S/http/www.cs.man.ac.uk/~pt/ASD/lamcra.pdf")
;; (find-lamcrapage 1)
;; (find-lamcratext)



;; «troelstra»  (to ".troelstra")
;; Anne Troelstra:
;; "Constructivism and Proof Theory":
;;   http://staff.science.uva.nl/~anne/eolss.pdf
;; "History of Constructivism in the 20th Century":
;;   http://staff.science.uva.nl/~anne/hhhist.pdf
(code-ps        "constrandpt" "$S/http/staff.science.uva.nl/~anne/eolss.pdf")
(code-pdftotext "constrandpt" "$S/http/staff.science.uva.nl/~anne/eolss.pdf")
;; (find-constrandptpage 1)
;; (find-constrandpttext)
;; (find-constrandptpage 17 "Topological and Algebraic Semantics")



;; «vistoli»  (to ".vistoli")
;; http://homepage.sns.it/vistoli/descent.pdf
(code-ps        "vistoli" "$S/http/homepage.sns.it/vistoli/descent.pdf")
(code-pdftotext "vistoli" "$S/http/homepage.sns.it/vistoli/descent.pdf")
;; (find-vistolipage 1)
;; (find-vistolitext)



;; «wadler»  (to ".wadler")
;; http://homepages.inf.ed.ac.uk/wadler/
;; http://homepages.inf.ed.ac.uk/wadler/papers/free/free.dvi
;; (find-sh0 "cd $S/http/homepages.inf.ed.ac.uk/wadler/papers/free/ && dvipdf free.dvi")
(code-dvi       "theoremsforfree" "$S/http/homepages.inf.ed.ac.uk/wadler/papers/free/free.dvi")
(code-pdftotext "theoremsforfree" "$S/http/homepages.inf.ed.ac.uk/wadler/papers/free/free.pdf")
;; (find-theoremsforfreepage 1)
;; (find-theoremsforfreetext)

;; "The Girard-Reynolds Isomorphism (second edition)"
;; http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html#gr2
;; http://homepages.inf.ed.ac.uk/wadler/papers/gr2/gr2.pdf
(code-ps        "wadlergriso" "$S/http/homepages.inf.ed.ac.uk/wadler/papers/gr2/gr2.pdf")
(code-pdftotext "wadlergriso" "$S/http/homepages.inf.ed.ac.uk/wadler/papers/gr2/gr2.pdf")
;; (find-wadlergrisopage 1)
;; (find-wadlergrisotext)

;; "Comprehending Monads"
;; http://homepages.inf.ed.ac.uk/wadler/papers/monads/monads.dvi
;; (find-sh0 "cd $S/http/homepages.inf.ed.ac.uk/wadler/papers/monads/ && dvipdf monads.dvi")
(code-dvi       "comprmonads" "$S/http/homepages.inf.ed.ac.uk/wadler/papers/monads/monads.dvi")
(code-pdftotext "comprmonads" "$S/http/homepages.inf.ed.ac.uk/wadler/papers/monads/monads.pdf")
;; (find-comprmonadspage 1)
;; (find-comprmonadstext)

;; King/Wadler: "Combining Monads"
;; http://homepages.inf.ed.ac.uk/wadler/papers/monadscomb/monadscomb.dvi
;; (find-sh0 "cd $S/http/homepages.inf.ed.ac.uk/wadler/papers/monadscomb/ && dvipdf monadscomb.dvi")
(code-dvi       "combmonads" "$S/http/homepages.inf.ed.ac.uk/wadler/papers/monadscomb/monadscomb.dvi")
(code-pdftotext "combmonads" "$S/http/homepages.inf.ed.ac.uk/wadler/papers/monadscomb/monadscomb.pdf")
;; (find-combmonadspage 1)
;; (find-combmonadstext)

;; "Monads for functional programming"
;; http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.dvi
;; http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf
(code-dvi       "monadsforfp" "$S/http/homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf")
(code-pdftotext "monadsforfp" "$S/http/homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf")
;; (find-monadsforfppage 1)
;; (find-monadsforfptext)





;; «winskel»  (to ".winskel")
;; "hocc" = "A Higher-Order Calculus for Categories"
;; http://www.brics.dk/RS/01/27/BRICS-RS-01-27.pdf
;; http://www.cl.cam.ac.uk/~gw104/catnotes.ps
(code-ps        "winskelhocc" "$S/http/www.brics.dk/RS/01/27/BRICS-RS-01-27.pdf")
(code-pdftotext "winskelhocc" "$S/http/www.brics.dk/RS/01/27/BRICS-RS-01-27.pdf")
(code-ps        "winskelcatnots" "$S/http/www.cl.cam.ac.uk/~gw104/catnotes.ps")
;; (find-winskelhoccpage 1)
;; (find-winskelhocctext)
;; (find-winskelcatnotspage 1)

;; «yanofsky»  (to ".yanofsky")
;; http://www.sci.brooklyn.cuny.edu/~noson/
;; http://www.sci.brooklyn.cuny.edu/~noson/paradox.pdf
(code-dvi       "diagonal" "$S/http/www.sci.brooklyn.cuny.edu/~noson/paradox.dvi")
(code-pdftotext "diagonal" "$S/http/www.sci.brooklyn.cuny.edu/~noson/paradox.pdf")
;; (find-diagonalpage 1)
;; (find-diagonaltext)








;; http://golem.ph.utexas.edu/category/2007/04/the_two_cultures_of_mathematic.html
;; http://www.math.uic.edu/~kauffman/Robbins.htm
;; http://www.dpmms.cam.ac.uk/~wtg10/2cultures.pdf
(code-ps        "twocultures" "$S/http/www.dpmms.cam.ac.uk/~wtg10/2cultures.pdf")
(code-pdftotext "twocultures" "$S/http/www.dpmms.cam.ac.uk/~wtg10/2cultures.pdf")
;; (find-twoculturespage 1)
;; (find-twoculturestext)
;; (find-twoculturestext "remembered")


;; Morten Sorensen / Pawel Urzyczyn: Lectures on the Curry-Howard Isomorphism
;; http://zls.mimuw.edu.pl/~urzy/ftp.html
;; ftp://ftp.mimuw.edu.pl/People/urzy/ch.ps.gz
(code-ps "urzy" "$S/ftp/ftp.mimuw.edu.pl/People/urzy/ch.ps.gz")
;; (find-urzypage 25  "Natural deduction")
;; (find-urzypage 89  "Type-chekcing and related problems")
;; (find-urzypage 105 "Sequent calculus")
;; (find-urzypage 143 "First-order logic")
;; (find-urzypage 155 "Dependent types")
;; (find-urzypage 191 "Second-order logic and polymorphism")
;; (find-urzypage 209 "The lambda-cube and pure type systems")
;; "a proper filter F is prime..."



;; http://math.unice.fr/~eugenia/catnotes/categorynotes-cheng.pdf
(code-ps        "echengcatnotes" "$S/http/math.unice.fr/~eugenia/catnotes/categorynotes-cheng.pdf")
(code-pdftotext "echengcatnotes" "$S/http/math.unice.fr/~eugenia/catnotes/categorynotes-cheng.pdf")
;; (find-echengcatnotespage 1)
;; (find-echengcatnotespage 45)
;; (find-echengcatnotespage 52 "Monads")
;; (find-echengcatnotestext)
;; (find-echengcatnotestext " 52\n\f")


;; http://citeseer.ist.psu.edu/197614.html

;; http://www.tac.mta.ca/tac/reprints/articles/16/tr16abs.html
;; http://www.tac.mta.ca/tac/reprints/articles/16/tr16.dvi




;; http://www.cs.kun.nl/~herman/Proefschrift.ps.gz
;;
(code-ps  "barbpi"
	 "$S/http/www.di.unito.it/~stefano/Barbanera-ProofIrrelevanceOutOf.ps")
(code-ps  "catcohlat" "$S/http/www.cs.nott.ac.uk/~rcb/MPC/CatTheory.ps.gz")
(code-ps  "cube" "$S/http/www.sato.kuis.kyoto-u.ac.jp/~takeuti/art/cube.ps.gz")
(code-dvi  "miraglia" "$S/http/www.ime.usp.br/~miraglia/public/tan.dvi")

;; (find-barbpipage 1)
;; (find-bdrgtpage (+ 1 78))
;; (find-catcohlatpage 2)
;; (find-diagxypage 1)
;; (find-miragliapage 203)
;; (find-cubepage 10)
;; (find-propstructpage 1)





;; http://www.cs.rhul.ac.uk/~zhaohui/books.html

;; ftp://iml.univ-mrs.fr/pub/ehrhard/difflamb.ps.gz

;; http://iml.univ-mrs.fr/~ehrhard/pub.html
;; http://iml.univ-mrs.fr/~ehrhard/pub/difflamb.pdf
(code-ps        "difflambda" "$S/http/iml.univ-mrs.fr/~ehrhard/pub/difflamb.pdf")
(code-pdftotext "difflambda" "$S/http/iml.univ-mrs.fr/~ehrhard/pub/difflamb.pdf")
;; (find-difflambdapage 1)
;; (find-difflambdatext)

(code-ps "rosolini" "-landscape $S/http/jazz.pst.informatik.uni-muenchen.de/spring-school99/topos.ps.gz")
(code-badpdf "lawvereSDG"
	     "$S/http/www.acsu.buffalo.edu/~wlawvere/SDG_Outline.pdf")
(code-ps "caccamo1" "$S/http/www.brics.dk/~mcaccamo/catnotes.ps.gz")
(code-dvi "caccamo2" "$S/http/www.brics.dk/RS/01/27/BRICS-RS-01-27.dvi.gz")
(code-ps "mcbridehole" "$S/http/www.dur.ac.uk/c.t.mcbride/diff.ps")
(code-dvi "moestacks" "$S/http/arxiv.org/ftp/math/papers/0212/0212266.dvi.gz")
(code-dvi "paradox" "$S/http/xxx.lanl.gov/abs/math.LO/0305282/paradox.dvi")





;; (find-difflambdapage 1)
;; (find-phoapage 1)
;; (find-rosolinipage 1)
;; (find-lawvereSDGpage 1)
;; (find-caccamo1page 1)
;; (find-caccamo2page 1)
;; (find-mcbrideholepage 1)
;; (find-moestackspage 1)
;; (find-paradoxpage 1)

;; (eev "cd $S/http/www.math.unipd.it/~maietti/papers/")
;; (find-millyarithpage 1)
(code-dvi "millyarith" "$S/http/www.math.unipd.it/~maietti/papers/aritbham.dvi")

;;