|
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")
;; «.altenkirch» (to "altenkirch")
;; «.atiyah» (to "atiyah")
;; «.avigad» (to "avigad")
;; «.awodey» (to "awodey")
;; «.barendregt» (to "barendregt")
;; «.barr» (to "barr")
;; «.beck» (to "beck")
;; «.beeson» (to "beeson")
;; «.bell» (to "bell")
;; «.benabou» (to "benabou")
;; «.beziau» (to "beziau")
;; «.birkedal» (to "birkedal")
;; «.blass» (to "blass")
;; «.blute» (to "blute")
;; «.butz» (to "butz")
;; «.corfield» (to "corfield")
;; «.cheng» (to "cheng")
;; «.dagostino» (to "dagostino")
;; «.day» (to "day")
;; «.depaiva» (to "depaiva")
;; «.dosen» (to "dosen")
;; «.dybjer» (to "dybjer")
;; «.eliasson» (to "eliasson")
;; «.farmer» (to "farmer")
;; «.fiore» (to "fiore")
;; «.freyd» (to "freyd")
;; «.fritz» (to "fritz")
;; «.gambino» (to "gambino")
;; «.geuvers» (to "geuvers")
;; «.girard» (to "girard")
;; «.goedel» (to "goedel")
;; «.grothendieck» (to "grothendieck")
;; «.gurevich» (to "gurevich")
;; «.hartshorne» (to "hartshorne")
;; «.hatcher» (to "hatcher")
;; «.henkin» (to "henkin")
;; «.hoare» (to "hoare")
;; «.hodges» (to "hodges")
;; «.hofmann» (to "hofmann")
;; «.hyland» (to "hyland")
;; «.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")
;; «.kock-dnc» (to "kock-dnc")
;; «.kondratiev» (to "kondratiev")
;; «.knuth» (to "knuth")
;; «.lakatos» (to "lakatos")
;; «.lamarche» (to "lamarche")
;; «.lamport» (to "lamport")
;; «.lang» (to "lang")
;; «.lawvere» (to "lawvere")
;; «.leinster» (to "leinster")
;; «.levy» (to "levy")
;; «.luo» (to "luo")
;; «.maclane» (to "maclane")
;; «.martin-lof» (to "martin-lof")
;; «.mckinna» (to "mckinna")
;; «.mckinsey» (to "mckinsey")
;; «.mjgabbay» (to "mjgabbay")
;; «.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")
;; «.seely-diff» (to "seely-diff")
;; «.shulman» (to "shulman")
;; «.simmons» (to "simmons")
;; «.simpson» (to "simpson")
;; «.street» (to "street")
;; «.streicher» (to "streicher")
;; «.stroustrup» (to "stroustrup")
;; «.taylor» (to "taylor")
;; «.townsend» (to "townsend")
;; «.troelstra» (to "troelstra")
;; «.urzyczyn» (to "urzyczyn")
;; «.vickers» (to "vickers")
;; «.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")
;; «.kopkadaly» (to "kopkadaly")
;; «.lamportlatex» (to "lamportlatex")
;; «.xypic» (to "xypic")
;; «.diagxy» (to "diagxy")
;; «.xfig» (to "xfig")
;; «.postscript» (to "postscript")
;; «.coq» (to "coq")
;; «.javascript» (to "javascript")
;; «.ruby» (to "ruby")
;; «.ruby-pragmatic» (to "ruby-pragmatic")
;; «.hp-laserjet-1300» (to "hp-laserjet-1300")
;; «.rmsessays» (to "rmsessays")
;; «.automath» (to "automath")
;; «.institutions» (to "institutions")
(defun +/2 (a b)
(/ (floor (+ a b)) 2))
;; «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."
;; «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)
;; «altenkirch» (to ".altenkirch")
;; Thorsten Altenkirch, 1999:
;; "Extensional Equality in Intensional Type Theory"
;; http://www.cs.nott.ac.uk/~txa/publ/
;; http://www.cs.nott.ac.uk/~txa/publ/lics99.pdf
(code-ps "exteqinitt" "$S/http/www.cs.nott.ac.uk/~txa/publ/lics99.pdf")
(code-pdftotext "exteqinitt" "$S/http/www.cs.nott.ac.uk/~txa/publ/lics99.pdf")
;; (find-exteqinittpage 1)
;; (find-exteqinittpage 8 "Categories with families as models of Type Theory")
;; (find-exteqinitttext)
;; «atiyah» (to ".atiyah")
;; (find-books "__alg/__alg.el" "atiyahmacdonald")
(code-djvu "atiyahmacdonald" "~/books/atiyah_macdonald__introduction_to_commutative_algebra.djvu")
;; (find-atiyahmacdonaldpage 4 "Contents")
;; (find-atiyahmacdonaldpage (+ 9 127) "Index")
;; «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)
;; «awodey» (to ".awodey")
;; (find-books "__cats/__cats.el" "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)
;; «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-books "__cats/__cats.el" "barr")
;; (find-LATEX "catsem.bib" "bib-BarrWells")
;; (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-beckthesispage 8 "tripleable")
;; (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")
;; «bell» (to ".bell")
;; J.L.Bell:
;; "Invitation to Smooth Infinitesimal Analysis"
;; http://publish.uwo.ca/~jbell/invitation%20to%20SIA.pdf
;; "Two Approaches to Modelling the Universe: SDG and Frame-Valued Sets"
;; http://publish.uwo.ca/~jbell/Two%20Approaches%20to%20Modelling%20the%20Universe.pdf
(code-ps "bellinvtosia" "$S/http/publish.uwo.ca/~jbell/invitation%20to%20SIA.pdf")
(code-pdftotext "bellinvtosia" "$S/http/publish.uwo.ca/~jbell/invitation%20to%20SIA.pdf")
(code-ps "belltwoatmtu" "$S/http/publish.uwo.ca/~jbell/Two%20Approaches%20to%20Modelling%20the%20Universe.pdf")
(code-pdftotext "belltwoatmtu" "$S/http/publish.uwo.ca/~jbell/Two%20Approaches%20to%20Modelling%20the%20Universe.pdf")
;; (find-bellinvtosiapage 1)
;; (find-bellinvtosiatext)
;; (find-belltwoatmtupage 1)
;; (find-belltwoatmtutext)
;; «benabou» (to ".benabou")
;; (find-LATEX "catsem.bib" "bib-Benabou")
;; Jean Bénabou: "Fibered Categories and the Foundations of Naive Category Theory"
;; http://www.jstor.org/stable/info/2273784
;; http://www.jstor.org/stable/pdfplus/2273784.pdf
(code-xpdf "benabou" "$S/http/www.jstor.org/stable/pdfplus/2273784.pdf")
(code-pdftotext "benabou" "$S/http/www.jstor.org/stable/pdfplus/2273784.pdf")
;; (find-benaboupage 1)
;; (find-benaboutext)
;; «beziau» (to ".beziau")
;; http://www.jyb-logic.org/start1.html
;; http://www.jyb-logic.org/papers.html
;; http://www.jyb-logic.org/S5.pdf
;; http://www.jyb-logic.org/jyb-wopalo-elsevier.pdf
(code-xpdf "beziauS5" "$S/http/www.jyb-logic.org/S5.pdf")
(code-pdftotext "beziauS5" "$S/http/www.jyb-logic.org/S5.pdf")
(code-xpdf "beziauplmodal" "$S/http/www.jyb-logic.org/jyb-wopalo-elsevier.pdf")
(code-pdftotext "beziauplmodal" "$S/http/www.jyb-logic.org/jyb-wopalo-elsevier.pdf")
;; (find-beziauS5page 1)
;; (find-beziauS5text "")
;; (find-beziauplmodalpage 1)
;; (find-beziauplmodaltext "")
;; «birkedal» (to ".birkedal")
;; Lars Birkedal's PhD thesis: "Developing Theories of Types and Computability via Realizability"
;; http://www.itu.dk/people/birkedal/papers/devttc.pdf
;; Biering/Birkedal/Torp-Smith: "BI-Hyperdoctrines, Higher-order Separation Logic, and Abstraction"
;; http://www.itu.dk/~birkedal/papers/hosl-journal.pdf
;; Birkedal/Mogelberg: "Categorical Models for Abadi/Plotkin's Logic for Parametricity"
;; http://www.itu.dk/~birkedal/papers/catmap.ps.gz
;; (find-sh "cd $S/http/www.itu.dk/~birkedal/papers/ && zcat catmap.ps.gz | ps2pdf - catmap.pdf")
(code-xpdf "birkedalthesis" "$S/http/www.itu.dk/people/birkedal/papers/devttc.pdf")
(code-pdftotext "birkedalthesis" "$S/http/www.itu.dk/people/birkedal/papers/devttc.pdf")
;; (find-birkedalthesispage 1 "Contents")
;; (find-birkedalthesispage (+ 1 1) "Index")
;; (find-birkedalthesistext "")
(code-ps "bihyp" "$S/http/www.itu.dk/~birkedal/papers/hosl-journal.pdf")
(code-pdftotext "bihyp" "$S/http/www.itu.dk/~birkedal/papers/hosl-journal.pdf")
;; (find-bihyppage 1)
;; (find-bihyptext)
(code-ps "cataplp" "$S/http/www.itu.dk/~birkedal/papers/catmap.ps.gz")
(code-xpdf "cataplp" "$S/http/www.itu.dk/~birkedal/papers/catmap.pdf")
;; (find-cataplppage 1)
;; «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)
;; «corfield» (to ".corfield")
;; (find-books "__phil/__phil.el" "corfield")
(code-ps "philrealmath" "~/books/__phil/corfield__towards_a_philosophy_of_real_mathematics.pdf")
(code-pdftotext "philrealmath" "~/books/__phil/corfield__towards_a_philosophy_of_real_mathematics.pdf")
;; (find-philrealmathpage 1)
;; (find-philrealmathtext)
;; (find-philrealmathtext "Just like Frege, the category theorist")
;; «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)
;; «dagostino» (to ".dagostino")
;; (find-es "math" "wdtp")
;; http://web.unife.it/utenti/marcello.dagostino/pubblicazioni.htm
;; http://logcom.oxfordjournals.org/cgi/reprint/4/3/285.pdf
;; D'Agostino/Mondadori: "The Taming of the Cut"
(code-xpdf "tamingofthecut" "$S/http/logcom.oxfordjournals.org/cgi/reprint/4/3/285.pdf")
(code-pdftotext "tamingofthecut" "$S/http/logcom.oxfordjournals.org/cgi/reprint/4/3/285.pdf")
;; (find-tamingofthecutpage 1)
;; (find-tamingofthecuttext)
;; «day» (to ".day")
;; http://www.math.mq.edu.au/~street/DayMasters.pdf
;; http://www.math.mq.edu.au/~street/DayPhD.pdf
(code-xpdf "dayphd" "$S/http/www.math.mq.edu.au/~street/DayPhD.pdf")
(code-xpdf "daymsc" "$S/http/www.math.mq.edu.au/~street/DayMasters.pdf")
;; (find-daymscpage 1)
;; (find-dayphdpage 1)
;; «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
;; «dosen» (to ".dosen")
;; Kosta Dosen: "Abstraction and Application in Adjunction"
;; http://arxiv.org/abs/math/0111061
;; http://arxiv.org/abs/math/0111061v1.dvi
;; http://arxiv.org/abs/math/0111061v1.pdf
(code-dvi "dosenaaadj" "$S/http/arxiv.org/abs/math/0111061v1.dvi")
(code-xpdf "dosenaaadj" "$S/http/arxiv.org/abs/math/0111061v1.pdf")
(code-pdftotext "dosenaaadj" "$S/http/arxiv.org/abs/math/0111061v1.pdf")
;; (find-dosenaaadjpage 1)
;; (find-dosenaaadjtext)
;; «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")
;; http://www.cl.cam.ac.uk/~mpf23/
;; http://www.cl.cam.ac.uk/~mpf23/Notes/psh.pdf
;; "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 9) "painfully difficult")
;; (find-freydabcatspage (+ 27 17))
;; (find-freydabcatspage (+ 27 39) "difference kernel")
;; (find-freydabcatspage (+ 27 47) "summation map")
;; «fritz» (to ".fritz")
;; Tobias Fritz: Categories of Fractions Revisited
;; http://arxiv.org/abs/0803.2587
;; http://arxiv.org/abs/0803.2587v1.dvi
;; http://arxiv.org/abs/0803.2587v1.pdf
;; (find-fline "$S/http/arxiv.org/abs/" "0803.2587")
;; (find-sh0 "mv -iv /tmp/0803.2587* $S/http/arxiv.org/abs/")
(code-dvi "fractions" "$S/http/arxiv.org/abs/0803.2587v1.dvi")
(code-xpdf "fractions" "$S/http/arxiv.org/pdf/0803.2587v1.pdf")
(code-pdftotext "fractions" "$S/http/arxiv.org/pdf/0803.2587v1.pdf")
;; (find-fractionspage 1)
;; (find-fractionstext)
;; «gambino» (to ".gambino")
;; Nicola Gambino's PhD thesis:
;; "Sheaf Interpretations for Generalised Predicative Intuitionistic Systems"
;; http://www.cs.le.ac.uk/people/ngambino/Publications/thesis.pdf
(code-ps "gambinothesis" "$S/http/www.cs.le.ac.uk/people/ngambino/Publications/thesis.pdf")
(code-pdftotext "gambinothesis" "$S/http/www.cs.le.ac.uk/people/ngambino/Publications/thesis.pdf")
;; (find-gambinothesispage 1)
;; (find-gambinothesispage 31)
;; (find-gambinothesistext)
;; (find-gambinothesistext "2.4.1 Categories of classes, abstractly")
;; «geuvers» (to ".geuvers")
;; http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz
;; http://www.cs.ru.nl/~herman/PUBS/IntroTT.pdf
;; http://www.cs.ru.nl/~herman/PUBS/gd.pdf
;;
;; 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")
;; (find-LATEX "catsem.bib" "bib-GLT")
;; 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-xpdf "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)
;; «hartshorne» (to ".hartshorne")
(code-djvu "hartshorne" "~/books/hartshorne__algebraic_geometry.djvu")
;; (find-hartshornepage (+ 1 1))
;; (find-hartshornepage 11 "Contents")
;; (find-hartshornepage (+ 18 1) "Contents")
;; (find-hartshornepage (+ 18 472) "Glossary of notations")
;; (find-hartshornepage (+ 18 478) "Index")
;; «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)
;; «hyland» (to ".hyland")
;; http://www.dpmms.cam.ac.uk/~martin/Research/Publications/publications.html
;; http://www.dpmms.cam.ac.uk/~martin/Research/Oldpapers/oldpapers.html
;; http://www.dpmms.cam.ac.uk/~martin/Research/Slides/slides.html
;; http://www.dpmms.cam.ac.uk/~martin/Research/Slides/bonn07.pdf
;; Hyland/Power: "The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads"
;; http://www.dpmms.cam.ac.uk/~martin/Research/Publications/2007/hp07.pdf
(code-xpdf "hpltm" "$S/http/www.dpmms.cam.ac.uk/~martin/Research/Publications/2007/hp07.pdf")
(code-pdftotext "hpltm" "$S/http/www.dpmms.cam.ac.uk/~martin/Research/Publications/2007/hp07.pdf")
;; (find-hpltmpage 1)
;; (find-hpltmtext)
;; Hyland: "The Effective Topos" (1982)
;; http://www.dpmms.cam.ac.uk/~martin/Research/Oldpapers/effectivetopos.pdf
(code-xpdf "hylandefftopos" "$S/http/www.dpmms.cam.ac.uk/~martin/Research/Oldpapers/effectivetopos.pdf")
;; (find-hylandefftopospage 1)
;; «jacobs» (to ".jacobs")
;; (find-books "__cats/__cats.el" "jacobs")
;; Bart Jacobs: "Categorical Logic and Type Theory"
(code-djvu "jacobs" "~/books/__cats/jacobs__categorical_logic_and_type_theory.djvu")
;; 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)
;; (find-jacobspage 8 "Contents")
;; (find-jacobspage (+ 19 1) "0_ Prospectus")
;; (find-jacobspage (+ 19 72) "1.7 Categories of fibrations")
;; (find-jacobspage (+ 19 119) "2_ Simple type theory")
;; (find-jacobspage (+ 19 169) "3_ Equational logic")
;; (find-jacobspage (+ 19 219) "4_ First order predicate logic")
;; (find-jacobspage (+ 19 282) "4.7_ Quotient types")
;; (find-jacobspage (+ 19 290) "4.7_ Quotient types, categorically")
;; «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 (+ 4 7) "Contents")
;; (find-jmthesispage (+ 4 23) "The birth of paraconsistent logic")
;; (find-jmthesistext "\n\nThe birth of paraconsistent logic")
;; (find-jmthesispage (+ 4 67) "Appendix: Brief historical note")
;; (find-jmthesistext "\n\nAppendix: Brief historical note")
;; (find-jmthesispage (+ 72 1) "Chapter One")
;; (find-jmthesistext "\fChapter One")
;; (find-jmthesistext)
;; «johnstone» (to ".johnstone")
;; (find-angg "books/__cats/__cats.el" "johnstone")
;; (find-LATEX "catsem.bib" "bib-Johnstone")
(code-djvu "topostheory" "~/books/__cats/johnstone__topos_theory.djvu")
(code-djvu "stonespaces" "~/books/__cats/johnstone__stone_spaces.djvu")
(code-djvu "elephant" "~/books/__cats/johnstone__sketches_of_an_elephant_2vols.djvu")
;;
;; (find-topostheorypage 7 "Contents")
;; (find-topostheorypage (+ 24 6) "0.18. (calculus of right fractions)")
;; (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-stonespacespage 3 "Contents")
;; (find-stonespacespage (+ 20 27) "complete Boolean algebra")
;; (find-stonespacespage (+ 20 31) "free complete lattice on three generators")
;; (find-stonespacespage (+ 20 169) "V. 1. A Crash Course in Sheaf Theory")
;; (find-stonespacespage (+ 20 324) "Bibliography")
;; (find-stonespacespage (+ 20 364) "Index of categories")
;; (find-stonespacespage (+ 20 366) "Index of other symbols")
;; (find-stonespacespage (+ 20 368) "Index of Definitions")
;;
;; (find-elephantpage 13 "Contents")
;; (find-elephantpage (+ 17 6) "Lambek" "Lemma 1.1.4" "initial object (A,\aa)")
;; (find-elephantpage (+ 17 11) "cartesian functor")
;; (find-elephantpage (+ 17 69) "logical functor")
;; (find-elephantpage (+ 17 84) "Example 2.1.3 [The filterquotient construction]")
;; (find-elephantpage (+ 17 161) "A4 Geometric Morphisms - Basic Theory")
;; (find-elephantpage (+ 17 264) "B1.3 Fibred Categories")
;; (find-elephantpage (+ 17 265) "prone")
;; (find-elephantpage (+ 17 471) "C1.1 Frames and Nuclei")
;; (find-elephantpage (+ 17 490) "neighbourhood filter")
;; (find-elephantpage (+ 15 828) "D1.3 First order logic")
;; (find-elephantpage (+ 15 841) "D1.4 Syntactic categories")
;; (find-elephantpage (+ 15 940) "D4.1 Interpreting higher-order logic in a topos")
;; (find-elephantpage (+ 15 951) "D4.2 Lambda-calculus and cartesian-closed categories")
;; (find-elephantpage (+ 15 952) "logic-free")
;; (find-elephantpage (+ 15 963) "D4.3 Toposes as type theories")
;; (find-elephantpage (+ 15 1032) "D4.7.17" "The Dedekind unit interval is a terminal coalgebra")
;; (find-elephantpage (+ 1104 1) "Bibiliography")
;; (find-elephantpage (+ 1104 55) "Index of Notation")
;; (find-elephantpage (+ 1104 61) "General Index")
;; "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
;; http://www.maths.usyd.edu.au/u/AusCat/speakers/lack.html
;; http://www.maths.usyd.edu.au/u/AusCat/abstracts/970409sl.html
(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")
;; (find-LATEX "catsem.bib" "bib-Kock77")
;; 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-kocksdgpage 5 "Contents")
;; (find-kocksdgtext 5 "Contents")
;; (find-kocksdgpage (+ 12 2) "I.1 Basic structure on the geometric line")
;; (find-kocksdgtext "I.1 Basic structure on the geometric line")
;; (find-kocksdgpage (+ 12 96) "PART II\nCategorical logic")
;; (find-kocksdgtext "PART II\nCategorical logic")
;; (find-kocksdgpage (+ 12 107) "II.4 Semantics of function objects" "X->R^D")
;; (find-kocksdgpage (+ 12 112) "II.5 Axiom 1 revisited")
;; (find-kocksdgpage (+ 12 227) "Index")
;; (find-kocksdgtext "Index")
;; (find-kocksdgtext)
;; Synthetic Geometry of Manifolds:
;; http://home.imf.au.dk/kock/SGMbeta.pdf
(code-ps "kocksgm" "$S/http/home.imf.au.dk/kock/SGMbeta.pdf")
(code-pdftotext "kocksgm" "$S/http/home.imf.au.dk/kock/SGMbeta.pdf")
;; (find-kocksgmpage 1)
;; (find-kocksgmtext)
;; 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)
;; «kock-dnc» (to ".kock-dnc")
;; (find-TH "2007dnc-sdg")
;; (find-books "__analysis/__analysis.el" "courant")
(code-xpdf "dnckock" "~/LATEX/2006nov26_kock77.pdf")
(code-pdftotext "dnckock" "~/LATEX/2006nov26_kock77.pdf")
;; (find-dnckockpage 1)
;; (find-dnckocktext)
;; (find-angg "LATEX/2008sdg.tex")
;; (find-dvipage "~/LATEX/2008sdg.dvi")
;; «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)
;; «knuth» (to ".knuth")
;; http://www-cs-faculty.stanford.edu/~knuth/fasc1a.ps.gz
(code-ps "knuthbits" "$S/http/www-cs-faculty.stanford.edu/~knuth/fasc1a.ps.gz")
;; (find-knuthbitspage 1 "Contents")
;; (find-knuthbitspage 109 "Index and Glossary")
;; «lakatos» (to ".lakatos")
(code-djvu "lakatos" "~/books/lakatos__proofs_and_refutations.djvu")
;; (find-lakatospage 3)
;; (find-lakatospage (+ 10 170))
;; «lamarche» (to ".lamarche")
;; http://www.loria.fr/~lamarche/
;; http://www.loria.fr/~lamarche/papers/NamingPrfsCL.pdf
(code-xpdf "lamarchenpcl" "http://www.loria.fr/~lamarche/papers/NamingPrfsCL.pdf")
(code-pdftotext "lamarchenpcl" "http://www.loria.fr/~lamarche/papers/NamingPrfsCL.pdf")
;; (find-lamarchenpclpage 1 "Contents")
;; (find-lamarchenpclpage (+ 1 1) "Index")
;; (find-lamarchenpcltext "")
;; «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)
;; «lang» (to ".lang")
(code-djvu "langalgebra" "~/books/lang__algebra_3rd_ed.djvu")
;; (find-langalgebrapage 10 "Contents")
;; (find-langalgebrapage (+ 15 92) "prime ideal")
;; (find-langalgebrapage (+ 15 377) "Chapter IX. Algebraic Spaces")
;; (find-langalgebrapage (+ 15 383) "generic point")
;; (find-langalgebrapage (+ 15 406) "Spec of a ring")
;; (find-langalgebrapage (+ 15 407) "Zariski topology")
;; (find-langalgebrapage (+ 15 408) "By a generic point of V in a field K")
;; (find-langalgebrapage (+ 15 903) "Index")
;; «lawvere» (to ".lawvere")
;; (find-books "__cats/__cats.el" "lawvere")
(code-djvu "lawvere70" "~/books/__cats/lawvere__equality_in_hyperdoctrines__1970.djvu")
;; (find-lawvere70page 2 "canonical natural isomorphisms")
;; (find-lawvere70page 6 "Substitutivity of equality")
;; (find-lawvere70page 8 "In any eed in which Frobenius Reciprocity and case (a) of the Beck condition holds,")
;; (find-lawvere70page 10 "In an eed in which Frobenius Reciprocity and Beck (b) hold,")
;; (find-lawvere70page 10 "where \theta is the ``middle four exchange isomorphism''")
;; (find-lawvere70page 12 "Comprehension Schema")
;; (find-lawvere70page 13 "then" "is an equalizer diagram")
;; 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/tr16abs.html
;; 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)
;; http://planetmath.org/encyclopedia/WilliamFrancisLawvere.html
(code-xpdf "lawveresfmaths" "~/books/lawvere__sets_for_mathematics.pdf")
;; (find-lawveresfmathspage 6 "Contents")
;; (find-lawveresfmathspage (+ 15 257) "Index")
;; 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:
;; http://www.cs.bham.ac.uk/~pbl/
;; http://www.cs.bham.ac.uk/~pbl/papers/
;; "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
;; http://www.tac.mta.ca/tac/volumes/14/5/14-05.pdf
(code-xpdf "cbpv" "$S/http/www.tac.mta.ca/tac/volumes/14/5/14-05.pdf")
(code-dvi "cbpv" "$S/http/www.tac.mta.ca/tac/volumes/14/5/14-05.dvi")
(code-pdftotext "cbpv" "$S/http/www.tac.mta.ca/tac/volumes/14/5/14-05.pdf")
;; (find-cbpvpage (+ -74 75))
;; (find-cbpvtext "")
;; "Call-By-Push-Value" (PhD thesis, 2001):
;; http://www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf
;; Book (parts): http://books.google.com/books?id=zas498825CkC
(code-xpdf "pblthesis" "$S/http/www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf")
(code-pdftotext "pblthesis" "$S/http/www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf")
;; (find-pblthesispage 1 "Contents")
;; (find-pblthesispage (+ 1 1) "Index")
;; (find-pblthesistext "")
;; "A tutorial on call-by-push-value" (slides):
;; http://www.cs.bham.ac.uk/~pbl/papers/cbpvefftt.pdf
(code-xpdf "pblslides" "$S/http/www.cs.bham.ac.uk/~pbl/papers/cbpvefftt.pdf")
(code-pdftotext "pblslides" "$S/http/www.cs.bham.ac.uk/~pbl/papers/cbpvefftt.pdf")
;; (find-pblslidespage 2 "Outline")
;; (find-pblslidespage 43 "Call-by-push-value types")
;; (find-pblslidespage 72 "Values and computations")
;; (find-pblslidespage 73 "Example program of type Fnat")
;; (find-pblslidestext "")
;; Lecture notes on Typed Lambda-Calculus (for the Midlands Graduate School):
;; 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")
;; «maclane» (to ".maclane")
;; (find-books "__cats/__cats.el" "maclane")
(code-xpdf "cwm" "~/books/__cats/maclane__CWM.pdf")
(code-djvu "cwm" "~/books/__cats/maclane__CWM_2up.djvu")
(code-djvu "cwm" "~/books/__cats/maclane__CWM_2up_b.djvu.djvu")
;; (find-cwmpage 3 "Table of Contents")
;; (find-cwmpage (+/2 6 133) "VI. Monads and Algebras")
;; (find-cwmpage (+/2 6 134) "VI. Monads and Algebras")
;; (find-cwmpage (+/2 3 253) "Index")
;; (find-cwmpage (+/2 3 254) "Index")
;; (find-cwmpage 3 "Table of Contents")
;; (find-cwmpage (+/2 6 133) "VI. Monads and Algebras")
;; (find-cwmpage (+/2 6 134) "VI. Monads and Algebras")
;; (find-cwmpage (+/2 6 147) "7. Beck's theorem")
;; (find-cwmpage (+/2 3 253) "Index")
;; (find-cwmpage (+/2 3 254) "Index")
;; «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)
;; «mckinna» (to ".mckinna")
;; James McKinna:
;; http://www.cs.ru.nl/~james/
;; Geuvers/McKinna/Wiedijk: "Pure Type Systems without Explicit Contexts"
;; http://www.cs.ru.nl/~james/2009-TLCA/submitted.pdf
;; McBride/McKinna 2004: "I am not a number: I am a free variable"
;; http://www.cs.st-andrews.ac.uk/~james/RESEARCH/notanum.pdf
;; McKinna/Pollack: "Pure Type Systems formalized":
;; http://www.cs.st-andrews.ac.uk/~james/RESEARCH/pts-formal.pdf
;; McKinna/Pollack: "Some Lambda-Calculus and Type Theory Formalized":
;; http://www.cs.st-andrews.ac.uk/~james/RESEARCH/jar99.pdf
(code-xpdf "gammainfty" "$S/http/www.cs.ru.nl/~james/2009-TLCA/submitted.pdf")
(code-pdftotext "gammainfty" "$S/http/www.cs.ru.nl/~james/2009-TLCA/submitted.pdf")
(code-xpdf "notanumber" "$S/http/www.cs.st-andrews.ac.uk/~james/RESEARCH/notanum.pdf")
(code-pdftotext "notanumber" "$S/http/www.cs.st-andrews.ac.uk/~james/RESEARCH/notanum.pdf")
(code-xpdf "ptsformalized" "$S/http/www.cs.st-andrews.ac.uk/~james/RESEARCH/pts-formal.pdf")
(code-pdftotext "ptsformalized" "$S/http/www.cs.st-andrews.ac.uk/~james/RESEARCH/pts-formal.pdf")
(code-xpdf "somalcattform" "$S/http/www.cs.st-andrews.ac.uk/~james/RESEARCH/jar99.pdf")
(code-pdftotext "somalcattform" "$S/http/www.cs.st-andrews.ac.uk/~james/RESEARCH/jar99.pdf")
;; (find-gammainftypage 1 "Contents")
;; (find-gammainftypage (+ 1 1) "Index")
;; (find-gammainftytext "")
;; (find-notanumberpage 1 "Contents")
;; (find-notanumberpage (+ 1 1) "Index")
;; (find-notanumbertext "")
;; (find-ptsformalizedpage 1 "Contents")
;; (find-ptsformalizedpage (+ 1 1) "Index")
;; (find-ptsformalizedtext "")
;; (find-somalcattformpage 1 "Contents")
;; (find-somalcattformpage (+ 1 1) "Index")
;; (find-somalcattformtext "")
;; «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)
;; «mjgabbay» (to ".mjgabbay")
;; http://www.gabbay.org.uk/papers.html
;; M.J.Gabbay, Martin Hofmann: "Nominal renaming sets"
;; http://www.gabbay.org.uk/papers/nomrs.pdf
;; M.J.Gabbay: "The Sets Foundations of Nominal Techniques"
;; http://www.gabbay.org.uk/papers/setfnt.pdf
(code-xpdf "nominalrensets" "$S/http/www.gabbay.org.uk/papers/nomrs.pdf")
(code-pdftotext "nominalrensets" "$S/http/www.gabbay.org.uk/papers/nomrs.pdf")
(code-xpdf "nominalfsets" "$S/http/www.gabbay.org.uk/papers/setfnt.pdf")
(code-pdftotext "nominalfsets" "$S/http/www.gabbay.org.uk/papers/setfnt.pdf")
;; (find-nominalrensetspage 1 "Contents")
;; (find-nominalrensetspage (+ 1 1) "Index")
;; (find-nominalrensetstext "")
;; (find-nominalfsetspage 1 "Contents")
;; (find-nominalfsetspage (+ 1 1) "Index")
;; (find-nominalfsetstext "")
;; «moerdijk» (to ".moerdijk")
;; (find-books "__cats/__cats.el" "moerdijk")
;; Moerdijk/Reyes: "Models for Smooth Infinitesimal Analysis" (book)
(code-djvu "moerey" "~/books/__cats/moerdijk_reyes__models_for_smooth_infinitesimal_analysis.djvu")
;; (find-moereypage 8 "Contents")
;; (find-moereypage (+ 9 24) "I.2. Manifolds as Cinfty-rings")
;; (find-moereypage (+ 9 27) "transversal")
;; (find-moereypage (+ 9 387) "Index")
;; «moggi» (to ".moggi")
;; http://www.disi.unige.it/person/MoggiE/publications.html
;; 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
;; http://www.disi.unige.it/person/MoggiE/ftp/abs-view.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")
(code-ps "moggiavpl" "$S/http/www.disi.unige.it/person/MoggiE/ftp/abs-view.pdf")
(code-pdftotext "moggiavpl" "$S/http/www.disi.unige.it/person/MoggiE/ftp/abs-view.pdf")
;; (find-moggifilterpage 1)
;; (find-moggifiltertext)
;; (find-moggiclcmpage 1)
;; (find-moggiclcmtext)
;; (find-moggincmpage 1)
;; (find-moggincmtext)
;; (find-moggiplosymppage 1)
;; (find-moggiplosymptext)
;; (find-moggiavplpage 1)
;; (find-moggiavpltext)
;; «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)
;; "Constructivist and Structuralist Foundations: Bishop's and Lawvere's Theories of Sets"
;; $S/http/www.math.uu.se/~palmgren/cetcs.pdf
(code-xpdf "palmgrencetcs" "$S/http/www.math.uu.se/~palmgren/cetcs.pdf")
(code-pdftotext "palmgrencetcs" "$S/http/www.math.uu.se/~palmgren/cetcs.pdf")
;; (find-palmgrencetcspage 1 "Contents")
;; (find-palmgrencetcstext "")
;; http://www.math.uu.se/~palmgren/cbhk-mscs.ps
;; (find-sh "cd $S/http/www.math.uu.se/~palmgren/ && ps2pdf cbhk-mscs.ps cbhk-mscs.pdf")
(code-xpdf "palmgrenbhk" "$S/http/www.math.uu.se/~palmgren/cbhk-mscs.pdf")
;; (find-palmgrenbhkpage 1 "Contents")
;; (find-palmgrenbhkpage (+ 1 1) "Index")
;; «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")
;; (find-LATEX "catsem.bib" "bib-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")
;; (find-LATEX "catsem.bib" "bib-SeelyBeck")
;; (find-LATEX "catsem.bib" "bib-SeelyCartDiff")
;; (find-LATEX "catsem.bib" "bib-SeelyDiff")
;; (find-LATEX "catsem.bib" "bib-SeelyLCCC")
;; (find-LATEX "catsem.bib" "bib-SeelyPLC")
;; 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 (+ -32 33))
;; (find-ragshyppage (+ -504 511) "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 (+ -967 969))
;; 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)
;; «seely-diff» (to ".seely-diff")
;; (find-TH "2007diffcats")
;; 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)
;; Cartesian Differential Categories (Blute / Cockett / Seely 2008):
;; http://www.math.mcgill.ca/rags/difftl/cartdiff.pdf
(code-ps "ragscartdiff" "$S/http/www.math.mcgill.ca/rags/difftl/cartdiff.pdf")
(code-pdftotext "ragscartdiff" "$S/http/www.math.mcgill.ca/rags/difftl/cartdiff.pdf")
;; (find-ragscartdiffpage 1)
;; (find-ragscartdiffpage 16)
;; (find-ragscartdifftext)
;; 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")
;; (find-streicherthesispage 1)
;; (find-streicherthesispage 9 "refute propositions which suspected to be underivable")
;; (find-streicherthesispage (+ 4 12) "Luo")
;; (find-streicherthesispage (+ 4 101) "3.6 Intensional Interpretations of N")
;; Thomas Streicher: "Introduction to Category Theory and Categorical Logic"
;; http://www.mathematik.tu-darmstadt.de/~streicher/CTCL.pdf.gz
;; (find-sh0 "cd $S/http/www.mathematik.tu-darmstadt.de/~streicher/ && zcat CTCL.pdf.gz > CTCL.pdf")
(code-xpdf "streicherctcl" "$S/http/www.mathematik.tu-darmstadt.de/~streicher/CTCL.pdf")
(code-pdftotext "streicherctcl" "$S/http/www.mathematik.tu-darmstadt.de/~streicher/CTCL.pdf")
;; (find-streicherctclpage 1 "Contents")
;; (find-streicherctclpage (+ 1 85) "13 Logic of Toposes")
;; (find-streicherctcltext "")
;; «stroustrup» (to ".stroustrup")
;; Reis/Stroustrup: "A Principled, Complete, and Efficient Representation"
;; http://www2.research.att.com/~bs/macis09.pdf
;; «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 84) "Beck condition")
;; (find-paultaylorthesispage (+ 11 84) "hyperdoctrine")
;; (find-paultaylorthesispage (+ 11 97) "(rules)")
;; (find-paultaylorthesispage (+ 11 101) "Indexed categories")
;; (find-paultaylorthesispage (+ 11 110) "non-cartesian subcategories")
;; (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)
;; «townsend» (to ".townsend")
;; http://www.christophertownsend.org/publications.htm
;; http://www.christophertownsend.org/Documents/townsendphd.pdf
;; See also: http://www.cs.bham.ac.uk/~sjv/papers.php
(code-xpdf "townsendphd" "$S/http/www.christophertownsend.org/Documents/townsendphd.pdf")
;; (find-townsendphdpage 4 "Contents")
;; (find-townsendphdpage (+ 1 24) "Directed subsets")
;; (find-townsendphdpage (+ 1 44) "Preframe")
;; (find-townsendphdpage (+ 1 153) "Index")
;; «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")
;; «urzyczyn» (to ".urzyczyn")
;; http://gigapedia.com/items/104040/lectures-on-the-curry-howard-isomorphism--volume-149--studies-in-logic-and-the-foundations-of-mathematics-
;; 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.dvi.gz
;; ftp://ftp.mimuw.edu.pl/People/urzy/ch.ps.gz
;; ftp://ftp.mimuw.edu.pl/People/urzy/ch.pdf
;; (find-sh0 "cd $S/ftp/ftp.mimuw.edu.pl/People/urzy/ && zcat ch.dvi.gz > ch.dvi && dvipdf ch.dvi")
(code-xpdf "urzy" "$S/ftp/ftp.mimuw.edu.pl/People/urzy/ch.pdf")
(code-dvi "urzy" "$S/ftp/ftp.mimuw.edu.pl/People/urzy/ch.dvi")
(code-pdftotext "urzy" "$S/ftp/ftp.mimuw.edu.pl/People/urzy/ch.pdf")
;; (find-urzypage (+ 12 25) "2.2. Natural deduction")
;; (find-urzypage (+ 12 35) "A proper filter F is prime iff")
;; (find-urzypage (+ 12 89) "6. Type-checking and related problems")
;; (find-urzypage (+ 12 105) "7. Sequent calculus")
;; (find-urzypage (+ 12 143) "9. First-order logic")
;; (find-urzypage (+ 12 155) "10. Dependent types")
;; (find-urzypage (+ 12 191) "12. Second-order logic and polymorphism")
;; (find-urzypage (+ 12 209) "13. The lambda-cube and pure type systems")
;; (find-urzytext)
;; «vickers» (to ".vickers")
;; http://www.cs.bham.ac.uk/~sjv/papers.php
;; Toposes pour les vraiment nuls:
;; http://www.cs.bham.ac.uk/~sjv/TopPLVN.pdf
;; Preframe presentations present:
;; http://www.cs.bham.ac.uk/~sjv/PreFrPrePre.pdf
(code-xpdf "topplvn" "$S/http/www.cs.bham.ac.uk/~sjv/TopPLVN.pdf")
(code-pdftotext "topplvn" "$S/http/www.cs.bham.ac.uk/~sjv/TopPLVN.pdf")
;; (find-topplvnpage 1)
;; (find-topplvntext "")
(code-xpdf "prefrprepre" "$S/http/www.cs.bham.ac.uk/~sjv/PreFrPrePre.pdf")
(code-pdftotext "prefrprepre" "$S/http/www.cs.bham.ac.uk/~sjv/PreFrPrePre.pdf")
;; (find-prefrpreprepage 1 "Contents")
;; (find-prefrpreprepage 3 "2. Essentially algebraic theories")
;; (find-prefrprepretext "")
;; «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)
;; (find-diagonalpage 18 "First Incompleteness Theorem")
;; (find-diagonaltext "First Incompleteness Theorem")
;; Noson S. Yanofsky:
;; "A Universal Approach to Self-Referential Paradoxes, Incompleteness
;; and Fixed Points" (preprint)
;; http://arxiv.org/abs/math/0305282
;; http://arxiv.org/abs/math/0305282.pdf
(code-xpdf "diagonalpre" "$S/http/arxiv.org/abs/math/0305282.pdf")
(code-pdftotext "diagonalpre" "$S/http/arxiv.org/abs/math/0305282.pdf")
;; (find-diagonalprepage 11 "Turing's halting problem")
;; (find-diagonalprepage 12 "hence no total Halt exists")
;; (find-diagonalprepage 16 "Godel's First Incompleteness Theorem")
;; (find-diagonalpretext "")
;; 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-xpdf "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")
;; 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")
;; http://research.microsoft.com/~gmb/Papers/tlca95.ps
(code-ps "bierman95" "$S/http/research.microsoft.com/~gmb/Papers/tlca95.ps")
;; (find-bierman95page 1)
;; «lua» (to ".lua")
;; http://www.tecgraf.puc-rio.br/~lhf/ftp/doc/jucs05.pdf
(code-xpdf "luaimp" "$S/http/www.tecgraf.puc-rio.br/~lhf/ftp/doc/jucs05.pdf")
(code-pdftotext "luaimp" "$S/http/www.tecgraf.puc-rio.br/~lhf/ftp/doc/jucs05.pdf")
;; (find-luaimppage 9)
;; (find-luaimppage 12)
;; (find-luaimptext)
;; (find-luaimptext "RK(X)")
;; (find-luaimptext "no-frills" "http://luaforge.net/docman/?group_id=83")
;; http://luaforge.net/docman/?group_id=83
;; http://luaforge.net/docman/view.php/83/98/ANoFrillsIntroToLua51VMInstructions.pdf
(code-xpdf "luanofrills" "$S/http/luaforge.net/docman/view.php/83/98/ANoFrillsIntroToLua51VMInstructions.pdf")
(code-pdftotext "luanofrills" "$S/http/luaforge.net/docman/view.php/83/98/ANoFrillsIntroToLua51VMInstructions.pdf")
;; (find-luanofrillspage 1)
;; (find-luanofrillspage 52 "Closures and Closing")
;; (find-luanofrillspage 54 "CLOSE")
;; (find-luanofrillstext)
;; http://www.paulgraham.com/onlisptext.html
;; http://www.paulgraham.com/lib/paulgraham/onlisp.pdf
;; http://lib.store.yahoo.net/lib/paulgraham/onlisp.ps.Z
(code-ps "onlisp" "$S/http/lib.store.yahoo.net/lib/paulgraham/onlisp.ps.Z")
(code-pdftotext "onlisp" "$S/http/www.paulgraham.com/lib/paulgraham/onlisp.pdf")
;; (find-onlisppage 12)
;; (find-onlisptext)
;; «coetzee» (to ".coetzee")
;; J.M. Coetzee: "The Lives of Animals" (1997)
;; 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-livesofanimalspage (+ -110 113))
;; (find-livesofanimalspage (+ -110 147) "Rilke's panther")
;; (find-livesofanimalstext)
;; (find-livesofanimalstext "147" "Rilke's panther")
;; (find-livesofanimalstext "127" "wrong thoughts")
;; (find-livesofanimalstext "132" "into the place of their victims")
;; (find-livesofanimalstext "134" "woke up haggard in the mornings")
;; (find-livesofanimalstext "143" "Babies have no self-consciousness")
;; (find-livesofanimalstext "145" "squirrel doing its thinking")
;; (find-livesofanimalstext "162" "a grasp of the meaning")
;; (find-livesofanimalstext "164" "last common ground")
;; "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."
;; «bentley» (to ".bentley")
;; (find-LATEX "catsem.bib" "Bentley")
;; Jon Bentley: "Little Languages" (CACM version)
;; http://classes.eclab.byu.edu/330/docs/p711-bentley.pdf
(code-xpdf "bentley" "$S/http/classes.eclab.byu.edu/330/docs/p711-bentley.pdf")
;; (find-bentleypage 1)
;; (find-bentleypage (+ -710 716) "CHEM")
;; «nassopoulos» (to ".nassopoulos")
;; George F. Nassopoulos
;; Note: the pdf urls below are artificial, the
;; author sent me the papers by e-mail...
;; http://users.uoa.gr/~gnassop/
;; http://users.uoa.gr/~gnassop/1.pdf
;; http://users.uoa.gr/~gnassop/2.pdf
;; http://users.uoa.gr/~gnassop/3.pdf
;; http://users.uoa.gr/~gnassop/4.pdf
;; http://users.uoa.gr/~gnassop/5.pdf
;; http://users.uoa.gr/~gnassop/6.pdf
;; http://users.uoa.gr/~gnassop/7.pdf
;; http://users.uoa.gr/~gnassop/8.pdf
;; http://users.uoa.gr/~gnassop/9.pdf
;; http://users.uoa.gr/~gnassop/bornologic.pdf
;; http://users.uoa.gr/~gnassop/spectral.pdf
;; (find-xpdfpage "$S/http/users.uoa.gr/~gnassop/1.pdf")
;; (find-xpdfpage "$S/http/users.uoa.gr/~gnassop/2.pdf")
;; (find-xpdfpage "$S/http/users.uoa.gr/~gnassop/3.pdf")
;; (find-xpdfpage "$S/http/users.uoa.gr/~gnassop/4.pdf")
;; (find-xpdfpage "$S/http/users.uoa.gr/~gnassop/5.pdf")
;; (find-xpdfpage "$S/http/users.uoa.gr/~gnassop/6.pdf")
;; (find-xpdfpage "$S/http/users.uoa.gr/~gnassop/7.pdf")
;; (find-xpdfpage "$S/http/users.uoa.gr/~gnassop/8.pdf")
;; (find-xpdfpage "$S/http/users.uoa.gr/~gnassop/9.pdf")
;; (find-pspage "$S/http/users.uoa.gr/~gnassop/spectral.pdf")
;; (find-pdftotext "$S/http/users.uoa.gr/~gnassop/spectral.pdf")
;; «profsoftdevel» (to ".profsoftdevel")
;; (find-es "omnisys" "profsoftdevel")
(code-c-d "profsoftdevel" "/tmp/profsoftdevel/" :ffox)
;; (find-profsoftdevelfile "")
;; (find-profsoftdevelw3m "0321193679_toc.html")
;; «tesemestr» (to ".tesemestr")
;; (find-es "tex" "tesemestr")
(code-c-d "tesemestr" "~/usrc/tesemestr/")
(code-c-d "slidesmestr" "~/usrc/tesemestr/slides/")
(code-c-d "2000uff" "~/usrc/tesemestr/uff/")
;; (find-tesemestrfile "")
;; (find-slidesmestrfile "")
;; (find-2000ufffile "")
;; http://angg.twu.net/math/
;; http://angg.twu.net/math/tesemestr.ps.gz
;; http://angg.twu.net/math/tesemestr.pdf
;; http://angg.twu.net/math/2000uff.ps.gz
(code-ps "tesemestr" "$S/http/angg.twu.net/math/tesemestr.ps.gz")
(code-pdftotext "tesemestr" "$S/http/angg.twu.net/math/tesemestr.pdf")
(code-ps "2000uff" "$S/http/angg.twu.net/math/2000uff.ps.gz")
(code-pdftotext "2000uff" "$S/http/angg.twu.net/math/2000uff.ps.gz")
;; (find-tesemestrpage 1)
;; (find-tesemestrtext)
;; (find-2000uffpage 1)
;; (find-2000ufftext)
;; «weber» (to ".weber")
;; Max Weber: "The Protestan Ethic and the Spirit of Capitalism"
;; http://www.ne.jp/asahi/moriyuki/abukuma/weber/world/ethic/pro_eth_frame.html
;; http://www.ne.jp/asahi/moriyuki/abukuma/weber/world/ethic/pro_eth_content.html
;; http://www.ne.jp/asahi/moriyuki/abukuma/weber/world/ethic/pro_eth_1.html
;; http://www.ne.jp/asahi/moriyuki/abukuma/weber/world/ethic/pro_eth_2.html
;; http://www.ne.jp/asahi/moriyuki/abukuma/weber/world/ethic/pro_eth_3.html
;; http://www.ne.jp/asahi/moriyuki/abukuma/weber/world/ethic/pro_eth_4.html
;; http://www.ne.jp/asahi/moriyuki/abukuma/weber/world/ethic/pro_eth_5.html
(code-c-d "webercap" "$S/http/www.ne.jp/asahi/moriyuki/abukuma/weber/world/ethic/")
;; (find-webercapw3m "pro_eth_content.html")
;; (find-webercapw3m "pro_eth_2.html")
;; (find-webercapw3m "pro_eth_2.html#ben-fra" "appearance of honesty")
;; (find-webercapw3m "pro_eth_2.html#rat-tra" "effectiveness")
;; (find-webercapw3m "pro_eth_2.html#ide-cal" "Philadelphia")
;; (find-webercapfile "pro_eth_2.html" "improvements in Philadelphia")
;; (find-webercapfile "")
;; http://www.math.uu.nl/people/jvoosten/realizability/history.ps.gz
;; http://www.math.uu.nl/people/jvoosten/syllabi/intuitionism.ps.gz
;; http://www.math.uu.nl/people/jvoosten/syllabi/toposmoeder.pdf
;; Jap van Oosten:
;; "Realizability: An Historical Essay" (2000)
;; http://www.math.uu.nl/people/jvoosten/realizability/history.ps.gz
;; (find-sh "cd $S/http/www.math.uu.nl/people/jvoosten/realizability/ && zcat history.ps.gz | ps2pdf - history.pdf")
(code-ps "realizabilityhistory" "$S/http/www.math.uu.nl/people/jvoosten/realizability/history.ps.gz")
(code-pdftotext "realizabilityhistory" "$S/http/www.math.uu.nl/people/jvoosten/realizability/history.pdf")
;; (find-realizabilityhistorypage 1)
;; (find-realizabilityhistorytext)
;; Halpern/Harper/Immerman/Kolaitis/Vardi/Vianu:
;; "On the Unusual Effectiveness of Logic in Computer Science" (2001)
;; (find-sh "cd $S/http/www.cs.rice.edu/~vardi/papers/ && zcat aaas99.jsl.ps.gz | ps2pdf - aaas99.jsl.pdf")
;; http://www.cs.rice.edu/~vardi/papers/aaas99.jsl.ps.gz
(code-ps "vardi" "$S/http/www.cs.rice.edu/~vardi/papers/aaas99.jsl.ps.gz")
(code-pdftotext "vardi" "$S/http/www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf")
;; (find-vardipage 1)
;; (find-varditext)
;; http://en.wikipedia.org/wiki/The_Unreasonable_Effectiveness_of_Mathematics_in_the_Natural_Sciences
;; http://www.dartmouth.edu/~matc/MathDrama/reading/Wigner.html
;; http://www.dartmouth.edu/~matc/MathDrama/reading/Hamming.html
;; Timothy Y. Chow - A beginner's guide to forcing
;; http://alum.mit.edu/www/tchow/forcing.pdf
(code-ps "forcing" "$S/http/alum.mit.edu/www/tchow/forcing.pdf")
(code-pdftotext "forcing" "$S/http/alum.mit.edu/www/tchow/forcing.pdf")
;; (find-forcingpage 1)
;; (find-forcingtext)
;; Sam Tobin-Hochstadt, Matthias Felleisen:
;; The Design and Implementation of Typed Scheme
;; http://www.ccs.neu.edu/scheme/pubs/popl08-thf.pdf
(code-ps "typedscheme" "$S/http/www.ccs.neu.edu/scheme/pubs/popl08-thf.pdf")
(code-pdftotext "typedscheme" "$S/http/www.ccs.neu.edu/scheme/pubs/popl08-thf.pdf")
;; (find-typedschemepage 1)
;; (find-typedschemetext)
;; Guide to the Software Engineering Body of Knowledge - Trial Version
;; SWEBOK - A Project of the Software Engineering Coordinating Committee
;; http://en.wikipedia.org/wiki/Software_configuration_management
;; http://www.swebok.org/stoneman/version_1.00/SWEBOK_w_correct_copyright_web_site_version.pdf
(code-xpdf "swebok" "$S/http/www.swebok.org/stoneman/version_1.00/SWEBOK_w_correct_copyright_web_site_version.pdf")
(code-pdftotext "swebok" "$S/http/www.swebok.org/stoneman/version_1.00/SWEBOK_w_correct_copyright_web_site_version.pdf")
;; (find-swebokpage 1)
;; (find-swebokpage (+ 22 103))
;; (find-sweboktext)
;; http://documentation.openoffice.org/manuals/oooauthors2/0113GS-WorkingWithStyles.pdf
(code-xpdf "oofficestyles" "$S/http/documentation.openoffice.org/manuals/oooauthors2/0113GS-WorkingWithStyles.pdf")
(code-pdftotext "oofficestyles" "$S/http/documentation.openoffice.org/manuals/oooauthors2/0113GS-WorkingWithStyles.pdf")
;; (find-oofficestylespage 1)
;; (find-oofficestylestext)
;; http://documentation.openoffice.org/manuals/oooauthors2/0100GS-GettingStarted.pdf
(code-xpdf "oofficegs" "$S/http/documentation.openoffice.org/manuals/oooauthors2/0100GS-GettingStarted.pdf")
(code-pdftotext "oofficegs" "$S/http/documentation.openoffice.org/manuals/oooauthors2/0100GS-GettingStarted.pdf")
;; (find-oofficegspage 1)
;; (find-oofficegspage 106)
;; (find-oofficegstext)
;; (find-oofficegspage (+ 10 119) "Draw")
;; András Kornai: Mathematical Linguistics
;; http://www.helsinki.fi/esslli/courses/readers/K54.pdf
;; "Typesetting in LaTeX endows a manuscript with an unfortunately
;; polished look, but in fact this is still an early draft, version
;; 0.56, ..."
(code-ps "mathling" "$S/http/www.helsinki.fi/esslli/courses/readers/K54.pdf")
(code-pdftotext "mathling" "$S/http/www.helsinki.fi/esslli/courses/readers/K54.pdf")
;; (find-mathlingpage 1)
;; (find-mathlingtext)
;; http://sevein.matap.uma.es/~aciego/mat-es/patrik.pdf
(code-ps "kleenemonads" "$S/http/sevein.matap.uma.es/~aciego/mat-es/patrik.pdf")
(code-pdftotext "kleenemonads" "$S/http/sevein.matap.uma.es/~aciego/mat-es/patrik.pdf")
;; (find-kleenemonadspage 1)
;; (find-kleenemonadstext)
;; http://www-maths.swan.ac.uk/staff/jrh/papers/JRHHislamWeb.pdf
(code-xpdf "histlc" "$S/http/www-maths.swan.ac.uk/staff/jrh/papers/JRHHislamWeb.pdf")
(code-ps "histlc" "$S/http/www-maths.swan.ac.uk/staff/jrh/papers/JRHHislamWeb.pdf")
(code-pdftotext "histlc" "$S/http/www-maths.swan.ac.uk/staff/jrh/papers/JRHHislamWeb.pdf")
;; (find-histlcpage 1)
;; (find-histlctext)
;; http://www.math.uni-sb.de/ag/wittstock/projekt2001.html
;; http://www.math.uni-sb.de/~ag-wittstock/OperatorSpace.pdf
(code-dvi "operatorspace" "$S/http/www.math.uni-sb.de/~ag-wittstock/OperatorSpace.dvi")
(code-pdftotext "operatorspace" "$S/http/www.math.uni-sb.de/~ag-wittstock/OperatorSpace.pdf")
;; (find-operatorspacepage 1)
;; (find-operatorspacetext)
;; David Metzler: Topological and Smooth Stacks
;; http://arxiv.org/pdf/math/0306176
;; http://arxiv.org/pdf/math/0306176.pdf
(code-ps "metzler" "$S/http/arxiv.org/pdf/math/0306176.pdf")
(code-pdftotext "metzler" "$S/http/arxiv.org/pdf/math/0306176.pdf")
;; (find-metzlerpage 5)
;; (find-metzlerpage 31)
;; (find-metzlertext "large site of a smooth manifold")
;; (find-metzlertext "manifolds as sheaves")
;; Steve Vickers: "Fuzzy Sets and Geometric Logic" (slides)
;; http://www.cs.bham.ac.uk/~sjv/LinzTalk.pdf
(code-ps "vickerslinz" "$S/http/www.cs.bham.ac.uk/~sjv/LinzTalk.pdf")
(code-xpdf "vickerslinz" "$S/http/www.cs.bham.ac.uk/~sjv/LinzTalk.pdf")
;; (find-vickerslinzpage 1)
;; (find-fline "~/LATEX/2008sheaves.tex")
(code-dvi "2008sheaves" "~/LATEX/2008sheaves.dvi")
;; (find-2008sheavespage 10)
(code-xpdf "dnckock" "~/LATEX/2006nov26_kock77.pdf")
(code-pdftotext "dnckock" "~/LATEX/2006nov26_kock77.pdf")
;; (find-dnckockpage 1)
;; (find-dnckocktext)
;; http://angg.twu.net/leatavora.html
;; http://angg.twu.net/leatavora/leatavora-tese.pdf
(code-ps "leatese" "$S/http/angg.twu.net/leatavora/leatavora-tese.pdf")
(code-pdftotext "leatese" "$S/http/angg.twu.net/leatavora/leatavora-tese.pdf")
;; (find-leatesepage 1)
;; (find-leatesepage 43 "A NEGAÇÃO HEGELIANA")
;; (find-leatesetext)
;; Kanovei/Shelah 2004: A definable nonstandard model of the reals
;; http://en.wikipedia.org/wiki/Hyperreal_number
;; http://shelah.logic.at/files/825.pdf
(code-xpdf "dnstmodel" "$S/http/shelah.logic.at/files/825.pdf")
(code-pdftotext "dnstmodel" "$S/http/shelah.logic.at/files/825.pdf")
;; (find-dnstmodelpage 1)
;; (find-dnstmodeltext)
;; Simon Thompson: "Type Theory and Functional Programming"
;; http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf
(code-ps "thompsonttfp" "$S/http/www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf")
(code-pdftotext "thompsonttfp" "$S/http/www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf")
;; (find-thompsonttfppage 1)
;; (find-thompsonttfptext)
;; (find-thompsonttfppage (+ 13 140) "A is a type is derivable from a : A")
;; (find-thompsonttfptext "5.4.1 A is a type is derivable from a : A")
;; SLNM 80: "Seminar on Triples and Categorical Homology Theory"
;; http://www.tac.mta.ca/tac/reprints/articles/18/tr18.dvi
;; http://www.tac.mta.ca/tac/reprints/articles/18/tr18.pdf
(code-dvi "seminarTCHT" "$S/http/www.tac.mta.ca/tac/reprints/articles/18/tr18.dvi")
(code-pdftotext "seminarTCHT" "$S/http/www.tac.mta.ca/tac/reprints/articles/18/tr18.pdf")
;; (find-seminarTCHTpage 1)
;; (find-seminarTCHTpage 46 "Linton")
;; (find-seminarTCHTpage 56 "Linton")
;; (find-seminarTCHTpage 95 "Jon Beck" "Distributive Laws")
;; (find-seminarTCHTpage 113 "Lawvere" "Ordinal Sums and Equational Doctrines")
;; (find-seminarTCHTtext)
;; http://crab.rutgers.edu/~pjohann/mscs05.pdf
(code-ps "johanncfree" "$S/http/crab.rutgers.edu/~pjohann/mscs05.pdf")
(code-pdftotext "johanncfree" "$S/http/crab.rutgers.edu/~pjohann/mscs05.pdf")
;; (find-johanncfreepage 1)
;; (find-johanncfreetext)
;; Jean Gallier: "Constructive Logics. Part I: A Tutorial on Proof Systems and Typed Lambda-Calculi"
;; ftp://ftp.cis.upenn.edu/pub/papers/gallier/conslog1.ps
;; (find-sh "cd $S/ftp/ftp.cis.upenn.edu/pub/papers/gallier/ && cat conslog1.ps | ps2pdf - conslog1.pdf")
(code-ps "gallier" "$S/ftp/ftp.cis.upenn.edu/pub/papers/gallier/conslog1.ps")
(code-pdftotext "gallier" "$S/ftp/ftp.cis.upenn.edu/pub/papers/gallier/conslog1.pdf")
;; (find-gallierpage 1)
;; (find-gallierpage 18 "Definition of the transformation")
;; (find-gallierpage 28 "First-Order Quantifiers")
;; (find-galliertext)
;; Francis Jeffry Pelletier: A History of Natural Deduction and
;; Elementary Logic Textbooks
;; http://www.sfu.ca/~jeffpell/papers/pelletierNDtexts.pdf
(code-ps "pelletier" "$S/http/www.sfu.ca/~jeffpell/papers/pelletierNDtexts.pdf")
(code-pdftotext "pelletier" "$S/http/www.sfu.ca/~jeffpell/papers/pelletierNDtexts.pdf")
;; (find-pelletierpage 1)
;; (find-pelletiertext)
;; Nuel Belnap: "Tonk, Plonk and Plink"
;; http://www.jstor.org/pss/3326862
(code-xpdf "tonkplonkplink" "~/tmp/Belnap_TonkPlonkPlink.pdf")
;; (find-tonkplonkplinkpage 1)
;; Nordström/Petersson/Smith:
;; "Programming in Martin-Löf's Type Theory - An Introduction"
;; http://www.cs.chalmers.se/Cs/Research/Logic/book/
;; http://www.cs.chalmers.se/Cs/Research/Logic/book/book.pdf
(code-ps "progmloftt" "$S/http/www.cs.chalmers.se/Cs/Research/Logic/book/book.pdf")
(code-pdftotext "progmloftt" "$S/http/www.cs.chalmers.se/Cs/Research/Logic/book/book.pdf")
;; (find-progmlofttpage 1)
;; (find-progmloftttext)
;; «bibtex» (to ".bibtex")
;; (find-es "tex" "bibtex")
;; (find-btxdocsh0 "cp -v btxdoc.dvi.gz /tmp/ && cd /tmp/ && gunzip -f btxdoc.dvi.gz && dvipdf btxdoc.dvi")
(code-c-d "btxdoc" "/usr/share/doc/tetex-doc/bibtex/base/")
(code-dvi "btxdoc" "/usr/share/doc/tetex-doc/bibtex/base/btxdoc.dvi.gz")
(code-pdftotext "btxdoc" "/tmp/btxdoc.pdf")
;; (find-btxdocpage 1)
;; (find-btxdoctext)
;; «memoirclass» (to ".memoirclass")
;; Peter Wilson: "The Memoir Class for Configurable Typesetting - User Guide"
;; http://www.ctan.org/tex-archive/macros/latex/contrib/memoir/memman.pdf
(code-ps "memoirclass" "$S/http/www.ctan.org/tex-archive/macros/latex/contrib/memoir/memman.pdf")
(code-pdftotext "memoirclass" "$S/http/www.ctan.org/tex-archive/macros/latex/contrib/memoir/memman.pdf")
;; (find-memoirclasspage 1)
;; (find-memoirclasspage (+ 34 51) "page layout parameters")
;; (find-memoirclasspage (+ 34 52) "page layout parameters")
;; (find-memoirclasspage (+ 34 61) "page layout parameters")
;; (find-memoirclasspage (+ 34 102) "layout parameters for general lists")
;; (find-memoirclasspage (+ 34 151) "float parameters")
;; (find-memoirclasstext)
;; «symbols» (to ".symbols")
;; http://www.ctan.org/tex-archive/info/symbols/comprehensive/
;; http://www.ctan.org/tex-archive/info/symbols/comprehensive/symbols-a4.pdf
;; http://www.ctan.org/tex-archive/info/symbols/comprehensive/source/symbols.tex
(code-ps "symbols" "$S/http/www.ctan.org/tex-archive/info/symbols/comprehensive/symbols-a4.pdf")
(code-pdftotext "symbols" "$S/http/www.ctan.org/tex-archive/info/symbols/comprehensive/symbols-a4.pdf")
;; (find-symbolspage 23)
;; (find-symbolstext)
;;
;; http://www.dimap.ufrn.br/pipermail/logica-l/2007-November/001842.html
;; (find-symbolspage 54)
;; (find-symbolstext " Table 193:")
;; http://centria.di.fct.unl.pt/~greg/latex/Symbols.pdf
(code-xpdf "gregsymbols" "$S/http/centria.di.fct.unl.pt/~greg/latex/Symbols.pdf")
(code-pdftotext "gregsymbols" "$S/http/centria.di.fct.unl.pt/~greg/latex/Symbols.pdf")
;; (find-gregsymbolspage 1)
;; (find-gregsymbolstext)
;; (find-es "tex" "stmaryrd")
(code-dvi "stmaryrd" "/usr/share/doc/texlive-math-extra/fonts/stmaryrd/stmaryrd.dvi.gz")
;; (find-stmaryrdpage 1)
;; «texbook» (to ".texbook")
;; (find-angg ".emacs" "find-texbookpage")
;; (find-eevex "tex.e" "find-texbookpage")
;; (find-es "tex" "texbook")
;; (find-texbookfile "")
(code-c-d "texbook" "~/usrc/texbook/")
(code-dvi "texbook" (ee-texbookfile "texbook.dvi"))
(code-pdftotext "texbook" (ee-texbookfile "texbook.pdf"))
;; (find-texbookfile "texbook.tex")
;; (find-texbookpage 9 "Contents")
;; (find-texbookpage (+ 11 457) "Index")
;; (find-texbooktext)
;; «mfbook» (to ".mfbook")
;; (find-es "tex" "mfbook")
;; (find-mfbookfile "")
(code-c-d "mfbook" "~/usrc/mfbook/")
(code-dvi "mfbook" (ee-mfbookfile "mfbook.dvi"))
(code-pdftotext "mfbook" (ee-mfbookfile "mfbook.pdf"))
;; (find-mfbookfile "mfbook.tex")
;; (find-mfbookpage 1)
;; (find-mfbooktext)
;; "User's Guide for the amsmath Package"
;; (find-fline (ee-amslmathfile ""))
;; (find-pspage (ee-amslmathfile "amsldoc.pdf"))
;; (find-pspage-links '(ee-amslmathfile "amsldoc.pdf"))
(code-ps "amsldoc" (ee-amslmathfile "amsldoc.pdf"))
(code-pdftotext "amsldoc" (ee-amslmathfile "amsldoc.pdf"))
;; (find-amsldocpage 1)
;; (find-amsldoctext)
;; «texbytopic» (to ".texbytopic")
;; Victor Eijkhout: "TeX by Topic, A TeXnician's Reference"
;; http://www.eijkhout.net/tbt/
;; http://www.cs.utk.edu/~eijkhout/texbytopic-a4.pdf
;; ftp://tug.ctan.org/pub/tex-archive/info/texbytopic/
;; ftp://tug.ctan.org/pub/tex-archive/info/texbytopic/TeXbyTopic.pdf
(code-ps "texbytopic" "$S/http/www.cs.utk.edu/~eijkhout/texbytopic-a4.pdf")
(code-pdftotext "texbytopic" "$S/http/www.cs.utk.edu/~eijkhout/texbytopic-a4.pdf")
(code-ps "texbytopic" "$S/ftp/tug.ctan.org/pub/tex-archive/info/texbytopic/TeXbyTopic.pdf")
(code-pdftotext "texbytopic" "$S/ftp/tug.ctan.org/pub/tex-archive/info/texbytopic/TeXbyTopic.pdf")
;; DVI version:
;; (find-es "tex" "texbytopic")
(code-c-d "texbytopic" "~/usrc/texbytopic/")
(code-dvi "texbytopic" (ee-texbytopicfile "TeXbyTopic.dvi"))
;; (find-texbytopicpage 1)
;; (find-texbytopictext)
;; (find-texbytopicpage (+ 1 170))
;; (find-texbytopictext "\nParagraph Shape")
;; (find-texbytopicpage (+ 1 173))
;; (find-texbytopictext "\\@hangfrom")
;; (find-texbytopictext "verbatim mode")
;; (find-texbytopicpage (+ 1 254) "\\newwrite")
;; (find-texbytopictext "\\newwrite")
;; (find-texbytopicpage (+ 1 26) "The visual processor")
;; (find-texbytopicpage (+ 1 53) "\\the\\font")
;; "The Visual LaTeX FAQ", by Scott Pakin
;; http://www.ctan.org/tex-archive/info/visualFAQ/
;; http://ctan.tug.org/get/info/visualFAQ/troubleshoot-vlf.pdf
;; http://ctan.tug.org/get/info/visualFAQ/visualFAQ.pdf
(code-xpdf "visuallatexfaq" "$S/http/ctan.tug.org/get/info/visualFAQ/visualFAQ.pdf")
(code-pdftotext "visuallatexfaq" "$S/http/ctan.tug.org/get/info/visualFAQ/visualFAQ.pdf")
;; (find-visuallatexfaqpage 1)
;; (find-visuallatexfaqtext)
(code-dvi "amsguide" "/usr/share/doc/tetex-doc/amstex/amsguide.dvi.gz")
;; (find-amsguidepage 1)
;; (find-amsguidepage 19 "\\ulcorner")
;; (find-amsguidepage 22 "\\pitchfork")
;; «lshort» (to ".lshort")
;; (find-es "tex" "lshort")
;; http://www.ctan.org/get/info/lshort/english/lshort.pdf
(code-ps "lshort" "$S/http/www.ctan.org/get/info/lshort/english/lshort.pdf")
(code-pdftotext "lshort" "$S/http/www.ctan.org/get/info/lshort/english/lshort.pdf")
(code-c-d "lshort" "~/usrc/lshort/")
;; (find-lshortpage 1)
;; (find-lshortpage (+ 14 92))
;; (find-lshortpage (+ 14 102))
;; (find-lshorttext)
;; (find-lshortfile "")
;; «kopkadaly» (to ".kopkadaly")
;; Kopka/Daly: "A Guide to LaTeX and Electronic Publishing (4th ed)"
(code-xpdf "kopkadaly4" "~/books/__comp/kopka_daly__a_guide_to_latex_4th_ed.pdf")
(code-pdftotext "kopkadaly4" "~/books/__comp/kopka_daly__a_guide_to_latex_4th_ed.pdf")
;; (find-kopkadaly4page 7 "Contents")
;; (find-kopkadaly4page (+ 12 3))
;; (find-kopkadaly4page (+ 12 33) "Page breaking")
;; (find-kopkadaly4page (+ 12 81) "4.6. Tabulator stops")
;; (find-kopkadaly4page (+ 12 97) "\\multicolumn")
;; (find-kopkadaly4page (+ 12 119) "Mathematical formulas")
;; (find-kopkadaly4page (+ 12 139) "eqarray")
;; (find-kopkadaly4page (+ 12 607) "Index")
;; (find-kopkadaly4text)
(defun kopka-daly-block ()
(interactive)
(insert "\
% (find-angg \".emacs.papers\" \"kopkadaly\")
% (find-kopkadaly4page 7 \"Contents\")
% (find-kopkadaly4page (+ 12 607) \"Index\")
% (find-kopkadaly4text)
"))
;; «lamportlatex» (to ".lamportlatex")
;; Leslie Lamport: "LaTeX - A Document Preparation System (2nd ed)"
(code-djvu "lamport" "~/books/__comp/lamport__latex_document_preparation_system.djvu")
;; (find-lamportpage 5 "Contents")
;; (find-lamportpage (+ 16 1))
;; (find-lamportpage (+ 17 237))
;; «xypic» (to ".xypic")
;; (find-zsh "dmissing xyrefer")
;; (find-zsh "dmissing xyguide")
(code-xpdf "xyrefer" "/usr/share/doc/texlive-pictures-doc/generic/xypic/xyrefer.pdf")
(code-pdftotext "xyrefer" "/usr/share/doc/texlive-pictures-doc/generic/xypic/xyrefer.pdf")
(code-xpdf "xyguide" "/usr/share/doc/texlive-doc/generic/xypic/xyguide.pdf")
(code-pdftotext "xyguide" "/usr/share/doc/texlive-doc/generic/xypic/xyguide.pdf")
;; (find-xyreferpage 2 "Contents")
;; (find-xyreferpage 17 "Figure 5: Kernel library <dir>ectionals")
;; (find-xyreferpage 78 "Index")
;; (find-xyrefertext "")
;; (find-xyguidepage 1 "Contents")
;; (find-xyguidepage (+ 1 1) "Index")
;; (find-xyguidetext "")
;; «diagxy» (to ".diagxy")
;; (find-es "xypic" "diagxy")
(code-c-d "diagxy" "~/usrc/diagxy/")
(code-dvi "diagxy" "~/usrc/diagxy/diaxydoc.dvi")
(code-pdftotext "diagxy" "~/usrc/diagxy/diaxydoc.pdf")
;; (find-diagxypage 25)
;; (find-diagxypage 18)
;; (find-diagxypage 30)
;; (find-diagxyfile "diaxydoc.tex" "subsection{Inline macros}")
;; (find-diagxytext)
;; «xfig» (to ".xfig")
;; (find-es "tex" "xfig")
(code-c-d "xfigref" "/usr/share/doc/xfig/html/")
(code-ps "xfigref" "/usr/share/doc/xfig/xfig_ref_en.pdf")
(code-pdftotext "xfigref" "/usr/share/doc/xfig/xfig_ref_en.pdf")
(code-ps "xfighowto" "/usr/share/doc/xfig/xfig-howto.pdf")
(code-pdftotext "xfighowto" "/usr/share/doc/xfig/xfig-howto.pdf")
;; (find-xfigrefpage 1)
;; (find-xfighowtopage 1)
;; «postscript» (to ".postscript")
;; (find-es "ps" "books")
;; http://partners.adobe.com/public/developer/en/ps/PLRM.pdf
;; http://www.adobe.com/devnet/postscript/
;; http://www.adobe.com/devnet/postscript/pdfs/PLRM.pdf
;; http://www.adobe.com/devnet/postscript/pdfs/PSerrata.txt
;; http://www.adobe.com/devnet/postscript/pdfs/PS3010and3011.Supplement.pdf
;; http://www.adobe.com/devnet/postscript/pdfs/5001.DSC_Spec.pdf
;; http://www.rightbrain.com/download/books/ThinkingInPostScript.pdf
(code-xpdf "pslr3" "$S/http/partners.adobe.com/public/developer/en/ps/PLRM.pdf")
(code-pdftotext "pslr3" "$S/http/partners.adobe.com/public/developer/en/ps/PLRM.pdf")
(code-ps "pslr3sup" "$S/http/www.adobe.com/devnet/postscript/pdfs/PS3010and3011.Supplement.pdf")
(code-pdftotext "pslr3sup" "$S/http/www.adobe.com/devnet/postscript/pdfs/PS3010and3011.Supplement.pdf")
(code-ps "psdscspec" "$S/http/www.adobe.com/devnet/postscript/pdfs/5001.DSC_Spec.pdf")
(code-pdftotext "psdscspec" "$S/http/www.adobe.com/devnet/postscript/pdfs/5001.DSC_Spec.pdf")
(code-xpdf "psthink" "$S/http/www.rightbrain.com/download/books/ThinkingInPostScript.pdf")
(code-pdftotext "psthink" "$S/http/www.rightbrain.com/download/books/ThinkingInPostScript.pdf")
(code-xpdf "psblue" "~/usrc/BlueBook/PSBlueBook.pdf")
(code-pdftotext "psblue" "~/usrc/BlueBook/PSBlueBook.pdf")
(code-c-d "psblue" "~/usrc/BlueBook/CODE/")
(code-xpdf "psgreen" "~/usrc/GreenBook/PSGreenBook.pdf")
(code-pdftotext "psgreen" "~/usrc/GreenBook/PSGreenBook.pdf")
(code-c-d "psgreen" "~/usrc/GreenBook/CODE/")
;; (find-pslr3page 1)
;; (find-pslr3text)
;; (find-pslr3text "print or =")
;; (find-pslr3text "(, ), <, >, [, ], {, }, /, and %")
;; (find-pslr3text "three conventions for quoting a literal string")
;; (find-pslr3text "[ and ]")
;; (find-pslr3text "{ and }")
;; (find-pslr3text "<< and >>")
;; (find-pslr3text "3.3.6 Packed Array Objects")
;; (find-pslr3text "3.4 Stacks")
;; (find-pslr3suppage 1)
;; (find-pslr3suptext)
;; (find-psdscspecpage 1)
;; (find-psdscspectext)
;; (find-psthinkpage 1)
;; (find-psthinktext)
;; (find-psbluepage 3 "Contents")
;; (find-psbluepage (+ 8 1) "1. Introduction")
;; (find-psbluepage (+ 7 7) "2. Stack and Arithmetic")
;; (find-psbluepage (+ 6 17) "3. Beginning Graphics")
;; (find-psbluepage (+ 4 35) "5. Printing Text")
;; (find-psbluepage (+ 4 47) "6. More Graphics")
;; (find-psbluepage (+ -4 241) "Index")
;; (find-psbluetext)
;; (find-psbluefile "")
;; (find-psgreenpage 2 "Contents")
;; (find-psgreenpage (+ 3 221) "Index")
;; (find-psgreentext)
;; (find-psgreenfile "")
;; «coq» (to ".coq")
;; (find-es "coq")
(code-ps "coqdocfaq" "/usr/share/doc/coq-doc-pdf/FAQ.v.pdf")
(code-pdftotext "coqdocfaq" "/usr/share/doc/coq-doc-pdf/FAQ.v.pdf")
(code-ps "coqdoctut" "/usr/share/doc/coq-doc-pdf/Tutorial.v.pdf")
(code-pdftotext "coqdoctut" "/usr/share/doc/coq-doc-pdf/Tutorial.v.pdf")
(code-ps "coqdocref" "/usr/share/doc/coq-doc-pdf/Reference-Manual.pdf")
(code-pdftotext "coqdocref" "/usr/share/doc/coq-doc-pdf/Reference-Manual.pdf")
(code-ps "coqdocrectut" "/usr/share/doc/coq-doc-pdf/RecTutorial.v.pdf")
(code-pdftotext "coqdocrectut" "/usr/share/doc/coq-doc-pdf/RecTutorial.v.pdf")
;; (find-coqdocfaqpage 1)
;; (find-coqdocfaqtext)
;; (find-coqdoctutpage 1)
;; (find-coqdoctuttext)
;; (find-coqdocrefpage 1)
;; (find-coqdocreftext)
;; (find-coqdocrectutpage 1)
;; (find-coqdocrectuttext)
;; Bertot/Casterán: "Interactive Theorem Proving and Program Development
;; (Coq'Art: The Calculus of Inductive Constructions)"
;; http://www.labri.fr/perso/casteran/CoqArt/index.html
;; http://www-sop.inria.fr/marelle/Yves.Bertot/research.html
;; http://gigapedia.com/items/123523/interactive-theorem-proving-and-program-development
(code-djvu "coqart" "~/books/__comp/bertot_casteran__interactive_theorem_proving_and_program_development.djvu")
;; (find-coqartpage 17 "Contents")
;; (find-coqartpage (+ 26 30) "2.3.2. Sections and Local Variables")
;; (find-coqartpage (+ 26 460) "Index")
;; «javascript» (to ".javascript")
;; (find-books "__comp/__comp.el" "crockford")
;; (find-es "javascript" "crockford")
(code-c-d "crockford" "~/usrc/crockford/final/")
;; (find-crockfordw3m "toc.html")
;; «ruby» (to ".ruby")
;; (find-es "ruby" "pragmatic")
;; (find-es "ruby" "ruby-in-a-nutshell")
;; (find-books "__comp/__comp.el" "ruby")
;; «hp-laserjet-1300» (to ".hp-laserjet-1300")
;; (find-es "print" "hp-laserjet-1300")
;; http://bizsupport1.austin.hp.com/bc/docs/support/SupportManual/bpl13095/bpl13095.pdf
(code-xpdf "hp1300userguide" "$S/http/bizsupport1.austin.hp.com/bc/docs/support/SupportManual/bpl13095/bpl13095.pdf")
(code-pdftotext "hp1300userguide" "$S/http/bizsupport1.austin.hp.com/bc/docs/support/SupportManual/bpl13095/bpl13095.pdf")
;; (find-hp1300userguidepage 1)
;; (find-hp1300userguidepage (+ 8 6) "Go button")
;; (find-hp1300userguidepage (+ 8 52) "Redistributing toner")
;; (find-hp1300userguidepage (+ 8 58) "Demo page")
;; (find-hp1300userguidepage (+ 8 58) "Configuration page")
;; (find-hp1300userguidepage (+ 8 70) "Finding the solution")
;; (find-hp1300userguidepage (+ 8 72) "Status light patterns")
;; (find-hp1300userguidepage (+ 8 89) "Clearing jams")
;; (find-hp1300userguidetext)
;; «rmsessays» (to ".rmsessays")
;; (find-es "texinfo" "rmsessays")
(code-c-d "rmsessays" "~/usrc/rms-essays/")
(code-dvi "rmsessays" "~/usrc/rms-essays/rms-essays.dvi")
(code-pdftotext "rmsessays" "~/usrc/rms-essays/rms-essays.pdf")
;; (find-rmsessayspage 1)
;; (find-rmsessayspage (+ 6 19) "printer")
;; (find-rmsessaystext "printer")
;; http://www.gnu.org/philosophy/words-to-avoid.html#Theft
;; (find-rmsessayspage (+ 6 206) "laws define justice or ethical conduct")
;; (find-rmsessaystext "laws define justice or ethical conduct")
;; (find-rmsessaystext)
;; Nathasha Alechina: "Functional Dependencies Between Variables"
;; http://www.cs.nott.ac.uk/~nza/studia.ps
;; (find-sh "cd $S/http/www.cs.nott.ac.uk/~nza/ && cat studia.ps | ps2pdf - studia.pdf")
(code-ps "navars" "$S/http/www.cs.nott.ac.uk/~nza/studia.ps")
(code-pdftotext "navars" "$S/http/www.cs.nott.ac.uk/~nza/studia.pdf")
;; (find-navarspage 1)
;; (find-navarstext)
;; Coquant/Huet: "The calculus of constructions" (1986)
;; http://www.inria.fr/rrrt/rr-0530.html
;; ftp://ftp.inria.fr/INRIA/publication/publi-pdf/RR/RR-0530.pdf
(code-pdftotext "coc86" "$S/ftp/ftp.inria.fr/INRIA/publication/publi-pdf/RR/RR-0530.pdf")
;; (find-coc86page 1)
;; XY-pic and notation for categorical diagrams
;; ftp://ftp.diku.dk/diku/semantics/papers/D-210.ps.Z
;; (find-sh "cd $S/ftp/ftp.diku.dk/diku/semantics/papers/ && zcat D-210.ps.Z | ps2pdf - D-210.pdf")
(code-ps "xycatd" "$S/ftp/ftp.diku.dk/diku/semantics/papers/D-210.ps.Z")
(code-pdftotext "xycatd" "$S/ftp/ftp.diku.dk/diku/semantics/papers/D-210.pdf")
;; (find-xycatdpage 1)
;; (find-xycatdtext)
;; Hassan Aït-Kaci: "Warren's Abstract Machine: a Tutorial Reconstruction"
;; http://wikix.ilog.fr/bin/view/Main/HassanAitKaci
;; http://www.vanx.org/archive/wam/wam.html
;; http://www.vanx.org/archive/wam/wambook.pdf
;; http://www.vanx.org/archive/wam/wam-slides.pdf
(code-ps "wambook" "$S/http/www.vanx.org/archive/wam/wambook.pdf")
(code-pdftotext "wambook" "$S/http/www.vanx.org/archive/wam/wambook.pdf")
(code-ps "wamslides" "$S/http/www.vanx.org/archive/wam/wam-slides.pdf")
(code-pdftotext "wamslides" "$S/http/www.vanx.org/archive/wam/wam-slides.pdf")
;; (find-wambookpage 1)
;; (find-wambooktext)
;; (find-wamslidespage 1)
;; (find-wamslidestext)
;; Norman Ramsey: "Teach Technical Writing in Two Hours per Week"
;; http://www.cs.tufts.edu/~nr/pubs/two-abstract.html
;; http://www.cs.tufts.edu/~nr/pubs/two.dvi
;; http://www.cs.tufts.edu/~nr/pubs/two.pdf
;; http://www.cs.tufts.edu/~nr/pubs/learn.dvi
;; http://www.cs.tufts.edu/~nr/pubs/learn.pdf
(code-dvi "nramseytwo" "$S/http/www.cs.tufts.edu/~nr/pubs/two.dvi")
(code-pdftotext "nramseytwo" "$S/http/www.cs.tufts.edu/~nr/pubs/two.pdf")
(code-dvi "nramseylearn" "$S/http/www.cs.tufts.edu/~nr/pubs/learn.dvi")
(code-pdftotext "nramseylearn" "$S/http/www.cs.tufts.edu/~nr/pubs/learn.pdf")
;; (find-nramseytwopage 1)
;; (find-nramseytwotext)
;; (find-nramseylearnpage 1)
;; (find-nramseylearntext)
;; Ieke Moerdijk/Benno van den Berg: "A Unified Approach to Algebraic Set Theory"
;; http://front.math.ucdavis.edu/0710.3066
;; http://front.math.ucdavis.edu/0710.3066.dvi
;; http://front.math.ucdavis.edu/0710.3066.pdf
(code-dvi "moeuast" "$S/http/front.math.ucdavis.edu/0710.3066.dvi")
(code-pdftotext "moeuast" "$S/http/front.math.ucdavis.edu/0710.3066.pdf")
;; (find-moeuastpage 1)
;; (find-moeuasttext)
;; Peter Freyd: "The Theory of Core Algebras: its Completeness"
;; http://www.tac.mta.ca/tac/volumes/18/11/18-11.dvi
;; http://www.tac.mta.ca/tac/volumes/18/11/18-11.pdf
(code-dvi "freydcore" "$S/http/www.tac.mta.ca/tac/volumes/18/11/18-11.dvi")
(code-pdftotext "freydcore" "$S/http/www.tac.mta.ca/tac/volumes/18/11/18-11.pdf")
;; (find-freydcorepage 1)
;; (find-freydcoretext)
;; Moerdijk: "Introduction to the Language of Stacks and Gerbes"
;; http://www.math.uu.nl/publications/preprints/1264.pdf
(code-ps "moestacks" "$S/http/www.math.uu.nl/publications/preprints/1264.pdf")
(code-pdftotext "moestacks" "$S/http/www.math.uu.nl/publications/preprints/1264.pdf")
;; (find-moestackspage 1)
;; (find-moestackstext)
;; Catherine Parent: "Synthese de preuves de programmes dans le Calcul des Constructions Inductives"
;; http://www-verimag.imag.fr/~parent/These/main.ps
;; (find-sh "cd $S/http/www-verimag.imag.fr/~parent/These/ && cat main.ps | ps2pdf - main.pdf")
(code-ps "parentphd" "$S/http/www-verimag.imag.fr/~parent/These/main.ps")
(code-pdftotext "parentphd" "$S/http/www-verimag.imag.fr/~parent/These/main.pdf")
;; (find-parentphdpage 1)
;; (find-parentphdtext)
;; Lopez-Escobar: "Equivalence Between Semantics for Intuitionism. I"
;; http://www.jstor.org/stable/info/2273226
;; http://www.jstor.org/stable/pdfplus/2273226.pdf
(code-xpdf "escobarebsi" "$S/http/www.jstor.org/stable/pdfplus/2273226.pdf")
(code-pdftotext "escobarebsi" "$S/http/www.jstor.org/stable/pdfplus/2273226.pdf")
;; (find-escobarebsipage 1)
;; (find-escobarebsitext)
;; J.L.Bell: "Isomorphism of Structures in S-Toposes"
;; http://www.jstor.org/stable/info/2273748
;; http://www.jstor.org/stable/pdfplus/2273748.pdf
(code-xpdf "bellisostrst" "$S/http/www.jstor.org/stable/pdfplus/2273748.pdf")
(code-pdftotext "bellisostrst" "$S/http/www.jstor.org/stable/pdfplus/2273748.pdf")
;; (find-bellisostrstpage 1)
;; (find-bellisostrsttext)
;; Boileau/Joyal: "La Logique des Topos"
;; http://www.jstor.org/stable/info/2273251
;; http://www.jstor.org/stable/pdfplus/2273251.pdf
(code-xpdf "boileaujoyal" "$S/http/www.jstor.org/stable/pdfplus/2273251.pdf")
(code-pdftotext "boileaujoyal" "$S/http/www.jstor.org/stable/pdfplus/2273251.pdf")
;; (find-boileaujoyalpage 1)
;; (find-boileaujoyaltext)
;; Barbara Veit: "A Proof of the Associated Sheaf Theorem by Means of Categorical Logic"
;; http://www.jstor.org/stable/info/2273255
;; http://www.jstor.org/stable/pdfplus/2273255.pdf
(code-xpdf "veit" "$S/http/www.jstor.org/stable/pdfplus/2273255.pdf")
(code-pdftotext "veit" "$S/http/www.jstor.org/stable/pdfplus/2273255.pdf")
;; (find-veitpage 1)
;; (find-veittext)
;; M.E.Szabo: review of "Model Theory and Topoi" (SLNM 445)
;; http://www.jstor.org/stable/info/2273267
;; http://www.jstor.org/stable/pdfplus/2273267.pdf
(code-xpdf "slnm445review" "$S/http/www.jstor.org/stable/pdfplus/2273267.pdf")
(code-pdftotext "slnm445review" "$S/http/www.jstor.org/stable/pdfplus/2273267.pdf")
;; (find-slnm445reviewpage 1)
;; (find-slnm445reviewtext)
;; http://www.oficinaraquel.com/casamentoblake.pdf
(code-xpdf "blaketmohah" "$S/http/www.oficinaraquel.com/casamentoblake.pdf")
;; (find-blaketmohahpage 1)
;; Arno Viero: "Russell on Peano's Axiomatization of Arithmetic"
;; http://www.analytica.inf.br/artigo.asp?ID=51&IDArt=95&IDNum=13
;; http://www.analytica.inf.br/95.pdf
(code-xpdf "arnopeano" "$S/http/www.analytica.inf.br/95.pdf")
(code-pdftotext "arnopeano" "$S/http/www.analytica.inf.br/95.pdf")
;; (find-arnopeanopage 1)
;; (find-arnopeanotext)
;; Equality in hyperdoctrines and comprehension schema as an adjoint functor (1970)
;; by F W Lawvere
;; Philippa Gardner:
;; "Equivalences between Logics and their Representing Type Theories"
;; http://www.doc.ic.ac.uk/~pg/papers/lf-full.ps.gz
;; (find-sh "cd $S/http/www.doc.ic.ac.uk/~pg/papers/ && zcat lf-full.ps.gz | ps2pdf - lf-full.pdf")
(code-ps "eqlrtt" "$S/http/www.doc.ic.ac.uk/~pg/papers/lf-full.ps.gz")
(code-pdftotext "eqlrtt" "$S/http/www.doc.ic.ac.uk/~pg/papers/lf-full.pdf")
;; (find-eqlrttpage 1)
;; (find-eqlrtttext)
;; Moura/Ierusalimschy: "Revisiting Coroutines" (2004)
;; http://www.inf.puc-rio.br/~roberto/docs/MCC15-04.pdf
(code-ps "revcoro" "$S/http/www.inf.puc-rio.br/~roberto/docs/MCC15-04.pdf")
(code-pdftotext "revcoro" "$S/http/www.inf.puc-rio.br/~roberto/docs/MCC15-04.pdf")
;; (find-revcoropage 1)
;; (find-revcorotext)
;; Jacques Carette:
;; Carette/Farmer: "High-Level Theories":
;; http://imps.mcmaster.ca/mathscheme/publications.html
;; http://imps.mcmaster.ca/doc/hlt.pdf
(code-ps "hlt" "$S/http/imps.mcmaster.ca/doc/hlt.pdf")
(code-pdftotext "hlt" "$S/http/imps.mcmaster.ca/doc/hlt.pdf")
;; (find-hltpage 1)
;; (find-hlttext)
;; Edmund Robinson: "Parametricity as Isomorphism"
;; http://www.dcs.qmw.ac.uk/~edmundr/publications.html
;; http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.5972
(code-ps "paramasiso" "~/tmp/10.1.1.55.5972.pdf")
(code-pdftotext "paramasiso" "~/tmp/10.1.1.55.5972.pdf")
;; (find-paramasisopage 1)
;; (find-paramasisotext)
;; http://www.cfh.ufsc.br/~dkrause/pg/livros/Logica/Rosto.pdf
(code-ps "krauselogasp" "$S/http/www.cfh.ufsc.br/~dkrause/pg/livros/Logica/Rosto.pdf")
(code-pdftotext "krauselogasp" "$S/http/www.cfh.ufsc.br/~dkrause/pg/livros/Logica/Rosto.pdf")
;; (find-krauselogasppage 1)
;; (find-krauselogasptext)
;; ftp://ftp.ipipan.gda.pl/andrzej/reports/set-theo-mod.ps.gz
;; http://ifile.it/yr6q4aj/concepts_techniques_and_models_of_compute_programming.rar
(code-ps "ctm" "~/tmp/concepts_techniques_and_models_of_computer_programming.pdf")
(code-pdftotext "ctm" "~/tmp/concepts_techniques_and_models_of_computer_programming.pdf")
;; (find-ctmpage 1)
;; (find-ctmpage (+ 31 308))
;; (find-ctmpage (+ 31 386))
;; (find-ctmtext)
;; http://www.math.mcgill.ca/rags/WkAdj/adj.pdf
(code-xpdf "seelywkadj" "$S/http/www.math.mcgill.ca/rags/WkAdj/adj.pdf")
;; (find-seelywkadjpage 1)
;; ftp://ftp.kestrel.edu/pub/papers/pavlovic/CLCI.ps
;; (find-sh "cd $S/ftp/ftp.kestrel.edu/pub/papers/pavlovic/ && cat CLCI.ps | ps2pdf - CLCI.pdf")
(code-ps "pavlovicclci" "$S/ftp/ftp.kestrel.edu/pub/papers/pavlovic/CLCI.ps")
(code-pdftotext "pavlovicclci" "$S/ftp/ftp.kestrel.edu/pub/papers/pavlovic/CLCI.pdf")
;; (find-pavlovicclcipage 1)
;; (find-pavlovicclcitext)
;; Bryan Ford: "Parsing Expression Grammars: A Recognition-Based Syntactic Foundation"
;; http://pdos.csail.mit.edu/~baford/packrat/popl04/peg-popl04.pdf
;; http://www.brynosaurus.com/pub/lang/peg-slides.pdf
(code-ps "pegford" "$S/http/pdos.csail.mit.edu/~baford/packrat/popl04/peg-popl04.pdf")
(code-pdftotext "pegford" "$S/http/pdos.csail.mit.edu/~baford/packrat/popl04/peg-popl04.pdf")
(code-xpdf "pegfordslides" "$S/http/www.brynosaurus.com/pub/lang/peg-slides.pdf")
;; (find-pegfordpage 1)
;; (find-pegfordtext)
;; (find-pegfordslidespage 1)
;; (find-xpdfpage "~/tmp/v6.pdf")
;; Timothy Speer: "A Short Study of Alexandroff Spaces"
;; http://arxiv.org/abs/0708.2136
(code-dvi "speeralexsp" "$S/http/arxiv.org/abs/0708.2136v1.dvi")
(code-pdftotext "speeralexsp" "$S/http/arxiv.org/abs/0708.2136v1.pdf")
;; (find-speeralexsppage 1)
;; (find-speeralexsptext)
;; Arenas: "Some results on Alexandroff Spaces"
;; http://at.yorku.ca/p/a/a/k/12.dvi
;; http://at.yorku.ca/p/a/a/k/12.htm
;; Uzcategui/Vielma: "Alexandroff Topologies viewed as closed sets in the Cantor Cube"
;; http://www.emis.de/journals/DM/v13-1/art5.pdf
;; Ying-Lie O: "Shape in Picture" (book)
;; http://books.google.com/books?id=-L_rCzK9fIsC
;; Dawar/Grohe/Kreutzer/Schweikardt: "Model theory makes formulas large"
;; http://www.newton.cam.ac.uk/preprints/NI07003.pdf
;; (find-sh "cd $S/http/www.newton.cam.ac.uk/preprints/ && zcat NI07003.pdf | ps2pdf - NI07003.pdf.pdf")
(code-ps "mtmfl" "$S/http/www.newton.cam.ac.uk/preprints/NI07003.pdf")
(code-pdftotext "mtmfl" "$S/http/www.newton.cam.ac.uk/preprints/NI07003.pdf")
;; (find-mtmflpage 1)
;; (find-mtmfltext)
;; J.H.Conway: "On Numbers and Games"
;; http://books.google.com/books?id=tXiVo8qA5PQC
;; Paul Taylor: "Practical Foundations of Mathematics"
;; http://books.google.com/books?id=C11Qnbjk200C
;; http://www.monad.me.uk/Practical-Foundations/
;; Johnstone: Stone Spaces
;; http://books.google.com/books?id=CiWwoLNbpykC
;; Martin Davis: "Engines of Logic - Mathematicians and the Origins of the Computer"
(code-djvu "daviseol" "~/books/davis_enginesoflogic.djvu")
;; (find-daviseolpage (+ 11 4))
;; Cirstea/Liquori/Wack: "Rewriting Calculus with Fixpoints: Untyped and First-order Systems"
;; http://rho.loria.fr/data/types2003.pdf
(code-ps "rhocalc2003" "$S/http/rho.loria.fr/data/types2003.pdf")
(code-pdftotext "rhocalc2003" "$S/http/rho.loria.fr/data/types2003.pdf")
;; (find-rhocalc2003page 1)
;; (find-rhocalc2003text)
;; van den Berg/Moerdijk: "W-types in sheaves"
;; http://arxiv.org/abs/0810.2398
;; http://arxiv.org/abs/0810.2398v1.dvi
;; http://arxiv.org/abs/0810.2398v1.pdf
;; (find-fline "$S/http/arxiv.org/abs/" "0810.2398")
;; (find-sh0 "mv -iv /tmp/0810.2398* $S/http/arxiv.org/abs/")
(code-dvi "wtypesinsheaves" "$S/http/arxiv.org/abs/0810.2398v1.dvi")
(code-xpdf "wtypesinsheaves" "$S/http/arxiv.org/abs/0810.2398v1.pdf")
(code-pdftotext "wtypesinsheaves" "$S/http/arxiv.org/abs/0810.2398v1.pdf")
;; (find-wtypesinsheavespage 1)
;; (find-wtypesinsheavestext)
;; Stephen Lack: "Notions of Lawvere theory"
;; http://arxiv.org/abs/0810.2578
;; http://arxiv.org/abs/0810.2578v1.dvi
;; http://arxiv.org/abs/0810.2578v1.pdf
;; (find-fline "$S/http/arxiv.org/abs/" "0810.2578")
;; (find-sh0 "mv -iv /tmp/0810.2578* $S/http/arxiv.org/abs/")
(code-dvi "lacknotionl" "$S/http/arxiv.org/abs/0810.2578v1.dvi")
(code-xpdf "lacknotionl" "$S/http/arxiv.org/abs/0810.2578v1.pdf")
(code-pdftotext "lacknotionl" "$S/http/arxiv.org/abs/0810.2578v1.pdf")
;; (find-lacknotionlpage 1)
;; (find-lacknotionltext)
;; Mark van Atten
;; http://isbndb.com/d/book/on_brouwer.html
;; http://www-ihpst.univ-paris1.fr/mvanatten
;; http://www.ozsl.uu.nl/brouwer/speaker-mva.html
;; http://www.cs.nyu.edu/pipermail/fom/2008-October/013121.html
;; http://www-ihpst.univ-paris1.fr/_sources/mvan_goedelbrouwer.pdf
;; Kaliszyk/Wiedijk/Hendriks/van Raamsdonk: "Teaching logic using a state-of-the-art proof assistant"
;; http://www.cs.vu.nl/~femke/ps/pate07.pdf
;; http://www.cs.vu.nl/~femke/ps/formed08.pdf
(code-xpdf "tluspa07" "$S/http/www.cs.vu.nl/~femke/ps/pate07.pdf")
(code-pdftotext "tluspa07" "$S/http/www.cs.vu.nl/~femke/ps/pate07.pdf")
(code-xpdf "tluspa08" "$S/http/www.cs.vu.nl/~femke/ps/formed08.pdf")
(code-pdftotext "tluspa08" "$S/http/www.cs.vu.nl/~femke/ps/formed08.pdf")
;; (find-tluspa07page 1)
;; (find-tluspa07text)
;; (find-tluspa08page 1)
;; (find-tluspa08text)
;; Noam Zeilberger: Focusing...
;; http://www.cs.cmu.edu/~noam/research.html
;; http://www.cs.cmu.edu/~noam/talks/LIX.28.02.08.pdf
;; Morten Rhiger: "Type-safe pattern combinators"
;; http://www.itu.dk/people/mir/typesafepatterns.pdf
;; Pavlovic: "Towards semantics of self-adaptive software"
;; http://www.comlab.ox.ac.uk/people/dusko.pavlovic/home.html
;; http://www.kestrel.edu/home/people/pavlovic/math.html
;; ftp://ftp.kestrel.edu/pub/papers/pavlovic/PavlovicD.bib
;; ftp://ftp.kestrel.edu/pub/papers/pavlovic/SSAS.ps
;; (find-sh "cd $S/ftp/ftp.kestrel.edu/pub/papers/pavlovic/ && cat SSAS.ps | ps2pdf - SSAS.pdf")
(code-ps "tssas" "$S/ftp/ftp.kestrel.edu/pub/papers/pavlovic/SSAS.ps")
(code-pdftotext "tssas" "$S/ftp/ftp.kestrel.edu/pub/papers/pavlovic/SSAS.pdf")
;; (find-tssaspage 1)
;; (find-tssastext)
;; ftp://ftp.kestrel.edu/pub/papers/pavlovic/mapsII.ps
;; (find-sh "cd $S/ftp/ftp.kestrel.edu/pub/papers/pavlovic/ && cat mapsII.ps | ps2pdf - mapsII.pdf")
(code-ps "pavmaps2" "$S/ftp/ftp.kestrel.edu/pub/papers/pavlovic/mapsII.ps")
(code-pdftotext "pavmaps2" "$S/ftp/ftp.kestrel.edu/pub/papers/pavlovic/mapsII.pdf")
;; (find-pavmaps2page 1)
;; (find-pavmaps2text)
;; Giuseppe Castagna:
;; http://www.pps.jussieu.fr/~gc/
;; http://www.di.ens.fr/users/castagna/
;; http://www.di.ens.fr/users/castagna/papers/icalp-ppdp05.pdf
;; http://www.pps.jussieu.fr/~gc/papers/semantic_subtyping.pdf
;; Joshua Dunfield: "A Unified System of Type Refinements"
;; http://www.cs.cmu.edu/~joshuad/papers/thesis/
;; http://www.cs.cmu.edu/~joshuad/papers/thesis/Dunfield07_Type_Refinements_thesis.pdf
(code-ps "typerefine" "$S/http/www.cs.cmu.edu/~joshuad/papers/thesis/Dunfield07_Type_Refinements_thesis.pdf")
(code-pdftotext "typerefine" "$S/http/www.cs.cmu.edu/~joshuad/papers/thesis/Dunfield07_Type_Refinements_thesis.pdf")
;; (find-typerefinepage 1)
;; (find-typerefinetext)
(code-xpdf "prawitz" "~/books/prawitz__natural_deduction.pdf")
;; (find-prawitzpage (+ -4 10))
;; (find-prawitzpage (+ -4 63))
(code-ps "intuitionandax" "~/books/intuition_and_the_axiomatic_method.pdf")
(code-pdftotext "intuitionandax" "~/books/intuition_and_the_axiomatic_method.pdf")
;; (find-intuitionandaxpage 1)
;; (find-intuitionandaxtext)
;; Bi-Heyting algebras, toposes and modalities (1996)
;; Gonzalo Reyes, Houman Zolfaghari
;; Journal of Philosophical Logic
;; http://citeseerx.ist.psu.edu/showciting?cid=920622
;; Topos-theoretic approaches to modality (1991)
;; Gonzalo Reyes, Houman Zolfaghari
;; SLNM 1488 - Category Theory (Como 1990) - 359-378
;; http://www.springerlink.com/content/1027277g8211685v/
;; Reyes, Reyes, Zolfaghari: Generic Figures and Their Glueings
;; http://books.google.com/books?id=Z5GcOhfwoD0C
;; http://www.amazon.com/Generic-figures-their-glueings-constructive/dp/8876990046/
;; Barry Hartley Slater: "The De-Mathematisation of Logic"
;; http://www.philosophy.uwa.edu.au/about/staff/hartley_slater/publications
;; http://www.polimetrica.com/main/list.php
(code-ps "demathl" "~/books/A100220f8TheDeMathematisationOfLogicOpenAccess.pdf")
(code-pdftotext "demathl" "~/books/A100220f8TheDeMathematisationOfLogicOpenAccess.pdf")
;; ~/books/__logic/slater__the_demathematisation_of_logic__openaccess.pdf
;; (find-demathlpage 1)
;; (find-demathlpage 217)
;; (find-demathltext)
;; http://www.clas.ufl.edu/users/jzeman/modallogic/chapter11.htm
;; Goubault-Larrecq/Goubault: "On the Geometry of Intuitionistic S4 Proofs"
;; http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2001-8.rr.ps
;; (find-sh "cd $S/http/www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ && cat rr-lsv-2001-8.rr.ps | ps2pdf - rr-lsv-2001-8.rr.pdf")
(code-ps "geomofis4proofs" "$S/http/www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2001-8.rr.ps")
(code-pdftotext "geomofis4proofs" "$S/http/www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2001-8.rr.pdf")
;; (find-geomofis4proofspage 1)
;; (find-geomofis4proofstext)
;; McLarty: "The Uses and Abuses of the History of Topos Theory" (1990)
;; http://bjps.oxfordjournals.org/cgi/content/abstract/41/3/351
;; http://en.wikipedia.org/wiki/Ultrafilter_lemma
;; B. Banaschewski, The Power of the Ultrafilter Theorem, Journal of
;; the London Mathematical Society (2) 27, 193--202, 1983.
;; http://journals.cambridge.org/action/displayJournal?jid=JLM
;; J. Halpern, The independence of the axiom of choice from the
;; Boolean prime ideal theorem, Fund. Math. 55, 57-66, 1964.
;; Larissa MacFarquhar: "The Devil's Accountant"
;; "Noam Chomsky's criticism of America's role in the world has
;; increased his isolation - and his audience."
;; http://www.newyorker.com/archive/2003/03/31/030331fa_fact_macfarquhar
;; Nikolaj Skallerud Bjorner: "Minimal Typing Derivations"
;; ftp://ftp.inria.fr/INRIA/Projects/cristal/MLworkshop94/13-bjorner.ps.Z
;; (find-sh "cd $S/ftp/ftp.inria.fr/INRIA/Projects/cristal/MLworkshop94/ && zcat 13-bjorner.ps.Z | ps2pdf - 13-bjorner.pdf")
(code-ps "minimaltyping" "$S/ftp/ftp.inria.fr/INRIA/Projects/cristal/MLworkshop94/13-bjorner.ps.Z")
(code-pdftotext "minimaltyping" "$S/ftp/ftp.inria.fr/INRIA/Projects/cristal/MLworkshop94/13-bjorner.pdf")
;; (find-minimaltypingpage 1)
;; (find-minimaltypingtext)
;; Royden: "Real Analysis"
(code-djvu "royden" "~/books/royden__real_analysis_3ed.djvu")
;; (find-roydenpage 9)
;; (find-roydenpage (+ 13 4))
;; van den Berg, Neves, eds: "The Strength of Non-Standard Analysis"
(code-djvu "strengthofnsa" "~/books/van_den_berg,_neves__the_strength_of_NSA.djvu")
;; (find-strengthofnsapage 12)
;; (find-strengthofnsapage (+ 18 3))
;; Conway: "On Numbers and Games"
(code-djvu "onag" "~/books/conway__on_numbers_and_games.djvu")
;; (find-onagpage 9)
;; (find-onagpage (+ 8 3))
;; (find-xpdf "~/books/goldblatt_modal.pdf")
;; http://standish.stanford.edu/bin/detail?fileID=1871730314
;; Modal logic and process algebra : a bisimulation perspective / Ponse, de Rijke, Venema, eds.
;; Derived Smooth Manifolds
;; Authors: David I. Spivak
;; http://arxiv.org/abs/0810.5174
(code-djvu "spivakcmans" "~/books/spivak__calculus_on_manifolds.djvu")
;; (find-spivakcmanspage 9 "Contents")
;; (find-spivakcmanspage (+ 12 141) "Index")
(code-djvu "gelfmanmhalg" "~/books/gelfand_manin__methods_of_homological_algebra.djvu")
;; (find-gelfmanmhalgpage 12 "Contents")
;; (find-gelfmanmhalgpage (+ 14 369) "Index")
;; «automath» (to ".automath")
;; (find-angg "books/__logic/__logic.el" "automath")
;; (find-books "__logic/__logic.el" "automath")
;; (find-books "__logic/__logic.el" "landau")
;; (find-LATEX "catsem.bib" "bib-Automath")
(code-xpdf "automath" "~/books/__logic/nederpelt__selected_papers_on_automath.pdf")
;; (find-automathpage 12 "Contents")
;; (find-automathpage (+ 21 1005) "Index of Subjects")
;; (find-automathpage (+ 21 3) "Twenty-Five Years of Automath Research")
;; (find-automathpage (+ 21 4) "In order to prevent the paradoxes")
;; (find-automathpage (+ 21 251) "Description of AUT-68")
;; (find-automathpage (+ 21 253) "PM (for ``primitive notion'')")
;; (find-automathpage (+ 21 268) "How to represent logic")
;; (find-automathpage (+ 21 57) "A.1 Verification of Mathematical Proofs by a Computer")
;; (find-automathpage (+ 21 127) "A.4 Formalization of Classical Mathematics in Automath")
;; (find-automathpage (+ 21 133) "Irrelevance of proofs")
;; (find-automathpage (+ 21 141) "A.5 A Survey of the Project Automath")
;; (find-automathpage (+ 21 201) "A.7 Reflections on Automath")
;; (find-automathpage (+ 21 229) "A.8 The Systems - Basic Ideas and Applications")
;; (find-automathpage (+ 21 687) "D.1 Example of a Text Written in Automath")
;; (find-automathpage (+ 21 701) "D.2 Checking Landau's Grundlagen in the Automath System")
;; (find-automathpage (+ 21 763) "Checking Landau's Grundlagen in the Automath System" "The PN-lines")
;; «institutions» (to ".institutions")
;; (find-es "ml" "twelf")
;; Goguen/Mossakowski/dePaiva/Rabe/Schröder "An Institutional View on Categorical Logic"
;; http://www.informatik.uni-bremen.de/~till/papers/CurryHoward.pdf
(code-xpdf "ivcl" "$S/http/www.informatik.uni-bremen.de/~till/papers/CurryHoward.pdf")
(code-pdftotext "ivcl" "$S/http/www.informatik.uni-bremen.de/~till/papers/CurryHoward.pdf")
;; (find-ivclpage 1 "Contents")
;; (find-ivclpage (+ 1 1) "Index")
;; (find-ivcltext)
;; http://kwarc.eecs.iu-bremen.de/frabe/
;; http://kwarc.eecs.iu-bremen.de/frabe/Research/phdthesis.pdf
(code-xpdf "rabephd" "$S/http/kwarc.eecs.iu-bremen.de/frabe/Research/phdthesis.pdf")
(code-pdftotext "rabephd" "$S/http/kwarc.eecs.iu-bremen.de/frabe/Research/phdthesis.pdf")
;; (find-rabephdpage 5 "Contents")
;; (find-rabephdpage 55 "Institutions")
;; (find-rabephdpage 33 "Preliminaries")
;; (find-rabephdpage (+ 1 1) "Index")
;; (find-rabephdtext)
;; http://www.cs.cornell.edu/home/rc/otherpublications.html
;; http://www.cs.cornell.edu/home/rc/documents/euroTICS.Zurich.2006.pdf
;; http://www.nuprl.org/documents/constable/recent.pdf
;; http://www.cs.bham.ac.uk/~vdp/publications/final-preface.pdf
;; http://kaivonfintel.org/publications/
;; http://mit.edu/fintel/www/modality.pdf
(code-ps "fintelmodlang" "$S/http/mit.edu/fintel/www/modality.pdf")
(code-pdftotext "fintelmodlang" "$S/http/mit.edu/fintel/www/modality.pdf")
;; (find-fintelmodlangpage 1)
;; (find-fintelmodlangtext)
;; Eilenberg/MacLane: "General Theory of Natural Equivalences", 1945
(code-xpdf "em45" "~/tmp/eilenberg_maclane__general_theory_of_natural_equivalences.pdf")
;; (find-em45page (+ -229 231) "Contents")
;; (find-em45page (+ -229 280) "Liting principle")
;; John Bourke: "The category of categories with pullbacks is cartesian closed"
;; http://arxiv.org/abs/0904.2486
;; http://arxiv.org/abs/0904.2486v1.dvi
;; http://arxiv.org/abs/0904.2486v1.pdf
;; (find-fline "$S/http/arxiv.org/abs/" "0904.2486")
;; (find-sh0 "mv -iv /tmp/0904.2486* $S/http/arxiv.org/abs/")
(code-dvi "catpbcc" "$S/http/arxiv.org/abs/0904.2486v1.dvi")
(code-xpdf "catpbcc" "$S/http/arxiv.org/abs/0904.2486v1.pdf")
(code-pdftotext "catpbcc" "$S/http/arxiv.org/abs/0904.2486v1.pdf")
;; (find-catpbccpage 1)
;; (find-catpbcctext)
;; http://books.google.com/books?id=sOLPNuxLC-wC The Authentic Life of Billy The Kid
;; (find-man "xpdf" "Set the zoom factor to 'page'")
;; Ralph Loader: Normalization by Calculation (1995)
;; http://homepages.ihug.co.nz/~suckfish/papers/normal.pdf
;; http://homepages.ihug.co.nz/~suckfish/papers/
;; http://homepages.ihug.co.nz/~suckfish/
;; Sally Haslanger: "Changing the Ideology and Culture of Philosophy: Not by Reason (Alone)"
;; http://www.mit.edu/~shaslang/papers/HaslangerCICP.pdf
;; http://crookedtimber.org/2007/09/06/sally-haslanger-on-women-in-philosophy/
(code-xpdf "haslanger" "$S/http/www.mit.edu/~shaslang/papers/HaslangerCICP.pdf")
(code-pdftotext "haslanger" "$S/http/www.mit.edu/~shaslang/papers/HaslangerCICP.pdf")
;; (find-haslangerpage 1 "Contents")
;; (find-haslangertext)
;; http://www.lsv.ens-cachan.fr/~markey/BibTeX/doc/ttb_en.pdf
(code-xpdf "tamethebst" "$S/http/www.lsv.ens-cachan.fr/~markey/BibTeX/doc/ttb_en.pdf")
(code-pdftotext "tamethebst" "$S/http/www.lsv.ens-cachan.fr/~markey/BibTeX/doc/ttb_en.pdf")
;; (find-tamethebstpage 1 "Contents")
;; (find-tamethebstpage (+ 1 1) "Index")
;; (find-tamethebsttext)
;; http://amath.colorado.edu/documentation/LaTeX/reference/faq/bibstyles.pdf
(code-xpdf "bibstyles" "$S/http/amath.colorado.edu/documentation/LaTeX/reference/faq/bibstyles.pdf")
(code-pdftotext "bibstyles" "$S/http/amath.colorado.edu/documentation/LaTeX/reference/faq/bibstyles.pdf")
;; (find-bibstylespage 1 "Contents")
;; (find-bibstylespage (+ 1 1) "Index")
;; (find-bibstylestext)
;; Russell O'Connor
;; "How to Understand What Classical Mathematicians Say" (slides):
;; http://www.cs.ru.nl/~spitters/completeness.html
;; http://www.cs.ru.nl/~spitters/completeness/OConnor.pdf
;; Adrian Mathias:
;; http://personnel.univ-reunion.fr/ardm/
;; "The Strength of Mac Lane Set Theory":
;; http://personnel.univ-reunion.fr/ardm/maclane.pdf
;; "The Ignorance of Bourbaki"
;; http://personnel.univ-reunion.fr/ardm/bourbaki.pdf
(code-xpdf "strengthofmac" "$S/http/personnel.univ-reunion.fr/ardm/maclane.pdf")
(code-pdftotext "strengthofmac" "$S/http/personnel.univ-reunion.fr/ardm/maclane.pdf")
;; (find-strengthofmacpage 3 "Contents")
;; (find-strengthofmacpage (+ 1 5) "Index")
;; (find-strengthofmactext "")
(code-xpdf "ignobourb" "$S/http/personnel.univ-reunion.fr/ardm/bourbaki.pdf")
(code-pdftotext "ignobourb" "$S/http/personnel.univ-reunion.fr/ardm/bourbaki.pdf")
;; (find-ignobourbpage 1 "Contents")
;; (find-ignobourbpage (+ 1 1) "Index")
;; (find-ignobourbtext "")
;; Bauer/Scott: "A New Category for Semantics"
;; http://www.cs.cmu.edu/Groups/LTC/index.html
;; http://www.cs.cmu.edu/Groups/LTC/papers/EQU.ps
;; http://www.cs.cmu.edu/Groups/LTC/papers/EQULogic_abstract.html
;; Wirth: "Compiler Construction"
;; http://en.wikipedia.org/wiki/P-code_machine
;; http://en.wikipedia.org/wiki/PL/0
;; http://www-old.oberon.ethz.ch/WirthPubl/CBEAll.pdf
(code-xpdf "wirthcc" "$S/http/www-old.oberon.ethz.ch/WirthPubl/CBEAll.pdf")
(code-pdftotext "wirthcc" "$S/http/www-old.oberon.ethz.ch/WirthPubl/CBEAll.pdf")
;; (find-wirthccpage 1 "Contents")
;; (find-wirthccpage (+ 1 1) "Index")
;; (find-wirthcctext "")
;; http://www.maths.mq.edu.au/~street/folkstring.pdf
;; (find-xpdfpage "$S/http/www.maths.mq.edu.au/~street/folkstring.pdf")
;; Hirschowitz/Maggesi: "Modules over Monads and Initial Semantics"
;; http://web.math.unifi.it/users/maggesi/syn.pdf
(code-xpdf "hirshmagsyn" "$S/http/web.math.unifi.it/users/maggesi/syn.pdf")
(code-pdftotext "hirshmagsyn" "$S/http/web.math.unifi.it/users/maggesi/syn.pdf")
;; (find-hirshmagsynpage 1 "Contents")
;; (find-hirshmagsynpage (+ 1 1) "Index")
;; (find-hirshmagsyntext "")
;; Ferreira/Oliva: "Functional Interpretations of Intuitionistic Linear Logic"
;; http://www.eecs.qmul.ac.uk/~gilda/article.pdf
;; http://www.eecs.qmul.ac.uk/~pbo/publications.html
(code-xpdf "ferrolfiill" "$S/http/www.eecs.qmul.ac.uk/~gilda/article.pdf")
(code-pdftotext "ferrolfiill" "$S/http/www.eecs.qmul.ac.uk/~gilda/article.pdf")
;; (find-ferrolfiillpage 1 "Contents")
;; (find-ferrolfiillpage (+ 1 1) "Index")
;; (find-ferrolfiilltext "")
;; Silva/Rutten: "A Coinductive Calculus of Binary Trees"
;; http://homepages.cwi.nl/~ams/publications/index.html
;; http://homepages.cwi.nl/~ams/publications/trees_extended.pdf
(code-xpdf "silvarutten" "$S/http/homepages.cwi.nl/~ams/publications/trees_extended.pdf")
(code-pdftotext "silvarutten" "$S/http/homepages.cwi.nl/~ams/publications/trees_extended.pdf")
;; (find-silvaruttenpage 1 "Contents")
;; (find-silvaruttenpage (+ 1 1) "Index")
;; (find-silvaruttentext "")
;; http://www.cs.brown.edu/~sk/Publications/Papers/Published/sk-automata-macros/
;; http://www.cs.brown.edu/~sk/Publications/Papers/Published/sk-automata-macros/paper.pdf
;; http://www.cs.brown.edu/~sk/Publications/Talks/SwineBeforePerl/
;; http://www.cs.brown.edu/~sk/Publications/Books/ProgLangs/2007-04-26/plai-2007-04-26.pdf
;; http://math.unice.fr/~carlos/themes/verif.html
;; http://hal.archives-ouvertes.fr/inria-00408143/
;; http://www.christophertownsend.org/
;;
;; Local Variables:
;; mode: emacs-lisp
;; coding: raw-text-unix
;; ee-delimiter-hash: "\n#*\n"
;; ee-delimiter-percent: "\n%*\n"
;; ee-anchor-format: "«%s»"
;; ee-comment-prefix: ";;"
;; End: