references.bib

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                                     %
% This is a database of documents referenced in mathlib file headers. %
%                                                                     %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

@article {MR1167694,
    AUTHOR = {Blass, Andreas},
     TITLE = {A game semantics for linear logic},
   JOURNAL = {Ann. Pure Appl. Logic},
  FJOURNAL = {Annals of Pure and Applied Logic},
    VOLUME = {56},
      YEAR = {1992},
    NUMBER = {1-3},
     PAGES = {183--220},
      ISSN = {0168-0072},
   MRCLASS = {03B70 (68Q55)},
  MRNUMBER = {1167694},
MRREVIEWER = {Fangmin Song},
       DOI = {10.1016/0168-0072(92)90073-9},
       URL = {https://doi.org/10.1016/0168-0072(92)90073-9},
}

@book {bourbaki1966,
    AUTHOR = {Bourbaki, Nicolas},
     TITLE = {Elements of mathematics. {G}eneral topology. {P}art 1},
 PUBLISHER = {Hermann, Paris; Addison-Wesley Publishing Co., Reading,
              Mass.-London-Don Mills, Ont.},
      YEAR = {1966},
     PAGES = {vii+437},
   MRCLASS = {54.00 (00.00)},
  MRNUMBER = {0205210},
}

@book {bourbaki1975,
    AUTHOR = {Bourbaki, Nicolas},
     TITLE = {Lie groups and {L}ie algebras. {C}hapters 1--3},
    SERIES = {Elements of Mathematics (Berlin)},
      NOTE = {Translated from the French,
              Reprint of the 1989 English translation},
 PUBLISHER = {Springer-Verlag, Berlin},
      YEAR = {1998},
     PAGES = {xviii+450},
      ISBN = {3-540-64242-0},
   MRCLASS = {17Bxx (00A05 22Exx)},
  MRNUMBER = {1728312},
}

@book {conway2001,
    AUTHOR = {Conway, J. H.},
     TITLE = {On numbers and games},
   EDITION = {Second},
 PUBLISHER = {A K Peters, Ltd., Natick, MA},
      YEAR = {2001},
     PAGES = {xii+242},
      ISBN = {1-56881-127-6},
   MRCLASS = {00A08 (05-01 91A05)},
  MRNUMBER = {1803095},
}

@book {gouvea1997,
    AUTHOR = {Gouv\^{e}a, Fernando Q.},
     TITLE = {{$p$}-adic numbers},
    SERIES = {Universitext},
   EDITION = {Second},
      NOTE = {An introduction},
 PUBLISHER = {Springer-Verlag, Berlin},
      YEAR = {1997},
     PAGES = {vi+298},
      ISBN = {3-540-62911-4},
   MRCLASS = {11S80 (11-01 12J25)},
  MRNUMBER = {1488696},
       DOI = {10.1007/978-3-642-59058-0},
       URL = {https://doi.org/10.1007/978-3-642-59058-0},
}

@book {james1999,
    AUTHOR = {James, Ioan},
     TITLE = {Topologies and uniformities},
    SERIES = {Springer Undergraduate Mathematics Series},
      NOTE = {Revised version of {{\i}t Topological and uniform spaces}
              [Springer, New York, 1987;  MR0884154 (89b:54001)]},
 PUBLISHER = {Springer-Verlag London, Ltd., London},
      YEAR = {1999},
     PAGES = {xvi+230},
      ISBN = {1-85233-061-9},
   MRCLASS = {54-01 (54A05 54E15)},
  MRNUMBER = {1687407},
MRREVIEWER = {Hans-Peter A. K\"{u}nzi},
       DOI = {10.1007/978-1-4471-3994-2},
       URL = {https://doi.org/10.1007/978-1-4471-3994-2},
}

@article {joyal1977,
 author = {André Joyal},
 title = {Remarques sur la théorie des jeux à deux personnes},
 journal = {Gazette des Sciences Mathematiques du Québec},
 volume = {1},
 number = {4},
 pages = {46--52},
 year = {1977},
 note = {(English translation at https://bosker.files.wordpress.com/2010/12/joyal-games.pdf)}
}

@inproceedings{lewis2019,
 author = {Lewis, Robert Y.},
 title = {A Formal Proof of {H}ensel's Lemma over the {$p$}-adic Integers},
 booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs},
 series = {CPP 2019},
 year = {2019},
 isbn = {978-1-4503-6222-1},
 location = {Cascais, Portugal},
 pages = {15--26},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/3293880.3294089},
 doi = {10.1145/3293880.3294089},
 acmid = {3294089},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Hensel's lemma, Lean, formal proof, p-adic},
}

@book {riehl2017,
   AUTHOR = {Riehl, Emily},
    TITLE = {Category theory in context},
PUBLISHER = {Dover Publications},
     YEAR = {2017},
     ISBN = {048680903X},
      URL = {http://www.math.jhu.edu/~eriehl/context.pdf},
}

@book{wall2018analytic,
  title={Analytic Theory of Continued Fractions},
  author={Wall, H.S.},
  isbn={9780486830445},
  series={Dover Books on Mathematics},
  year={2018},
  publisher={Dover Publications}
}

@article{ahrens2017,
 author = {Benedikt Ahrens and Peter LeFanu Lumsdaine},
   year = {2019},
  title = {Displayed Categories},
journal = {Logical Methods in Computer Science},
 volume = {15},
  issue = {1},
    doi = {10.23638/LMCS-15(1:20)2019},
}

@Book{HubbardWest-ode,
author = {John H. Hubbard and Beverly H. West},
title = {Differential Equations: A Dynamical Systems Approach},
subtitle = {Ordinary Differential Equations},
year = {1991},
publisher = {Springer},
location = {New York},
volume = {5},
isbn = {978-1-4612-8693-6},
doi = {10.1007/978-1-4612-4192-8},
pages = {XX, 350},
}

@book{borceux-vol1,
  title={Handbook of Categorical Algebra: Volume 1, Basic Category Theory},
  author={Borceux, Francis},
  series={Encyclopedia of Mathematics},
  volume={50},
  year={1994},
  publisher={Cambridge University Press}
}

@book{borceux-vol2,
  title={Handbook of Categorical Algebra: Volume 2, Categories and Structures},
  author={Borceux, Francis},
  series={Encyclopedia of Mathematics},
  volume={51},
  year={1994},
  publisher={Cambridge University Press}
}
@book {atiyah-macdonald,
    AUTHOR = {Atiyah, M. F. and Macdonald, I. G.},
     TITLE = {Introduction to commutative algebra},
 PUBLISHER = {Addison-Wesley Publishing Co., Reading, Mass.-London-Don
              Mills, Ont.},
      YEAR = {1969},
     PAGES = {ix+128},
   MRCLASS = {13.00},
  MRNUMBER = {0242802},
MRREVIEWER = {J. A. Johnson},
}

@book {soare1987,
    AUTHOR = {Soare, Robert I.},
     TITLE = {Recursively enumerable sets and degrees},
    SERIES = {Perspectives in Mathematical Logic},
      NOTE = {A study of computable functions and computably generated sets},
 PUBLISHER = {Springer-Verlag, Berlin},
      YEAR = {1987},
     PAGES = {xviii+437},
      ISBN = {3-540-15299-7},
   MRCLASS = {03-02 (03D20 03D25 03D30)},
  MRNUMBER = {882921},
MRREVIEWER = {Peter G. Hinman},
       DOI = {10.1007/978-3-662-02460-7}
}

@inproceedings{carneiro2019,
  author    = {Mario M. Carneiro},
  editor    = {John Harrison and
               John O'Leary and
               Andrew Tolmach},
  title     = {Formalizing Computability Theory via Partial Recursive Functions},
  booktitle = {10th International Conference on Interactive Theorem Proving, {ITP}
               2019, September 9-12, 2019, Portland, OR, {USA}},
  series    = {LIPIcs},
  volume    = {141},
  pages     = {12:1--12:17},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2019},
  url       = {https://doi.org/10.4230/LIPIcs.ITP.2019.12},
  doi       = {10.4230/LIPIcs.ITP.2019.12},
  timestamp = {Fri, 27 Sep 2019 15:57:06 +0200},
  biburl    = {https://dblp.org/rec/conf/itp/Carneiro19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}