flypitch-itp-2019.bib

@article{godel1938consistency,
  title={The consistency of the axiom of choice and of the generalized continuum-hypothesis},
  author={G{\"o}del, Kurt},
  journal={Proceedings of the National Academy of Sciences},
  volume={24},
  number={12},
  pages={556--557},
  year={1938},
  publisher={National Acad Sciences}
}

@inproceedings{paulson2008relative,
  author    = {Lawrence C. Paulson},
  title     = {The Relative Consistency of the Axiom of Choice - Mechanized Using
               Isabelle/ZF},
  booktitle = {Logic and Theory of Algorithms, 4th Conference on Computability in
               Europe, CiE 2008, Athens, Greece, June 15-20, 2008, Proceedings},
  pages     = {486--490},
  year      = {2008},
  crossref  = {DBLP:conf/cie/2008},
  url       = {https://doi.org/10.1007/978-3-540-69407-6\_52},
  doi       = {10.1007/978-3-540-69407-6\_52},
  timestamp = {Tue, 14 May 2019 10:00:41 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cie/Paulson08},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/cie/2008,
  editor    = {Arnold Beckmann and
               Costas Dimitracopoulos and
               Benedikt L{\"{o}}we},
  title     = {Logic and Theory of Algorithms, 4th Conference on Computability in
               Europe, CiE 2008, Athens, Greece, June 15-20, 2008, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5028},
  publisher = {Springer},
  year      = {2008},
  url       = {https://doi.org/10.1007/978-3-540-69407-6},
  doi       = {10.1007/978-3-540-69407-6},
  isbn      = {978-3-540-69405-2},
  timestamp = {Tue, 14 May 2019 10:00:41 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cie/2008},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{harrison1998formalizing,
  author    = {John Harrison},
  title     = {Formalizing Basic First Order Model Theory},
  booktitle = {Theorem Proving in Higher Order Logics, 11th International Conference,
               TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings},
  pages     = {153--170},
  year      = {1998},
  crossref  = {DBLP:conf/tphol/1998},
  url       = {https://doi.org/10.1007/BFb0055135},
  doi       = {10.1007/BFb0055135},
  timestamp = {Tue, 14 May 2019 10:00:48 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tphol/Harrison98},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/tphol/1998,
  editor    = {Jim Grundy and
               Malcolm C. Newey},
  title     = {Theorem Proving in Higher Order Logics, 11th International Conference,
               TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1479},
  publisher = {Springer},
  year      = {1998},
  url       = {https://doi.org/10.1007/BFb0055125},
  doi       = {10.1007/BFb0055125},
  isbn      = {3-540-64987-5},
  timestamp = {Tue, 14 May 2019 10:00:48 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tphol/1998},
  bibsource = {dblp computer science bibliography, https://dblp.org}
} 

@phdthesis{schlichtkrull2018formalization,
  title={Formalization of logic in the {Isabelle} proof assistant},
  author={Schlichtkrull, Anders},
  year={2018},
  school={Technical University of Denmark}
}

@article{braselmann1930godel,
  title={G{\"o}del’s Completeness Theorem1},
  author={Braselmann, Patrick and Koepke, Peter},
  journal={Monatshefte f{\"u}r Mathematik und Physik},
  volume={37},
  pages={349--360},
  year={1930}
}

@article{blanchette2017soundness,
  title={Soundness and completeness proofs by coinductive methods},
  author={Blanchette, Jasmin Christian and Popescu, Andrei and Traytel, Dmitriy},
  journal={Journal of automated reasoning},
  volume={58},
  number={1},
  pages={149--179},
  year={2017},
  publisher={Springer}
}

@article{godel1947cantor,
  title={What is Cantor's continuum problem?},
  author={G{\"o}del, Kurt},
  journal={The American Mathematical Monthly},
  volume={54},
  number={9},
  pages={515--525},
  year={1947},
  publisher={Taylor \& Francis}
}

@book{harrison2009handbook,
  author    = {John Harrison},
  title     = {Handbook of Practical Logic and Automated Reasoning},
  publisher = {Cambridge University Press},
  year      = {2009},
  isbn      = {978-0-521-89957-4},
  timestamp = {Tue, 08 Feb 2011 14:57:04 +0100},
  biburl    = {https://dblp.org/rec/bib/books/daglib/0022394},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{cohen-the-independence-of-the-continuum-hypothesis-1,
  title={The independence of the continuum hypothesis},
  author={Cohen, Paul J},
  journal={Proceedings of the National Academy of Sciences},
  volume={50},
  number={6},
  pages={1143--1148},
  year={1964},
  publisher={National Acad Sciences}
}

@phdthesis{ilik2010constructive,
  title={Constructive completeness proofs and delimited control},
  author={Ilik, Danko},
  year={2010},
  school={Ecole Polytechnique X}
}

@inproceedings{de2015lean,
  author    = {Leonardo Mendon{\c{c}}a de Moura and
               Soonho Kong and
               Jeremy Avigad and
               Floris van Doorn and
               Jakob von Raumer},
  title     = {The {Lean} Theorem Prover (System Description)},
  booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on
               Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
  pages     = {378--388},
  year      = {2015},
  crossref  = {DBLP:conf/cade/2015},
  url       = {https://doi.org/10.1007/978-3-319-21401-6\_26},
  doi       = {10.1007/978-3-319-21401-6\_26},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/MouraKADR15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/cade/2015,
  editor    = {Amy P. Felty and
               Aart Middeldorp},
  title     = {Automated Deduction - {CADE-25} - 25th International Conference on
               Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9195},
  publisher = {Springer},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-319-21401-6},
  doi       = {10.1007/978-3-319-21401-6},
  isbn      = {978-3-319-21400-9},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2015},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Ridge2005AMV,
  author    = {Tom Ridge and
               James Margetson},
  title     = {A Mechanically Verified, Sound and Complete Theorem Prover for First
               Order Logic},
  booktitle = {Theorem Proving in Higher Order Logics, 18th International Conference,
               TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings},
  pages     = {294--309},
  year      = {2005},
  crossref  = {DBLP:conf/tphol/2005},
  url       = {https://doi.org/10.1007/11541868\_19},
  doi       = {10.1007/11541868\_19},
  timestamp = {Tue, 14 May 2019 10:00:48 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tphol/RidgeM05},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/tphol/2005,
  editor    = {Joe Hurd and
               Thomas F. Melham},
  title     = {Theorem Proving in Higher Order Logics, 18th International Conference,
               TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3603},
  publisher = {Springer},
  year      = {2005},
  url       = {https://doi.org/10.1007/11541868},
  doi       = {10.1007/11541868},
  isbn      = {3-540-28372-2},
  timestamp = {Tue, 14 May 2019 10:00:48 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tphol/2005},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{FOL-Fitting-AFP,
  author  = {Stefan Berghofer},
  title   = {First-Order Logic According to {Fitting}},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2007,
  note    = {\url{http://isa-afp.org/entries/FOL-Fitting.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
 
@article{Completeness-AFP,
  author  = {James Margetson and Tom Ridge},
  title   = {Completeness theorem},
  journal = {Archive of Formal Proofs},
  month   = sep,
  year    = 2004,
  note    = {\url{http://isa-afp.org/entries/Completeness.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@misc{margetson2004proving,
  title={Proving the Completeness Theorem within Isabelle/HOL},
  author={Margetson, James},
  year={2004},
  publisher={Citeseer}
}

@book{shankar1997metamathematics,
  title={Metamathematics, machines and G{\"o}del's proof},
  author={Shankar, Natarajan},
  volume={38},
  year={1997},
  publisher={Cambridge University Press}
}

@inproceedings{shoenfield1971unramified,
  title={Unramified forcing},
  author={Shoenfield, Joseph R},
  booktitle={Axiomatic set theory},
  volume={13},
  pages={357--381},
  year={1971},
  organization={AMS Providence, RI}
}

@article{gunther2018first,
  author    = {Emmanuel Gunther and
               Miguel Pagano and
               Pedro S{\'{a}}nchez Terraf},
  title     = {First steps towards a formalization of Forcing},
  journal   = {CoRR},
  volume    = {abs/1807.05174},
  year      = {2018},
  url       = {http://arxiv.org/abs/1807.05174},
  archivePrefix = {arXiv},
  eprint    = {1807.05174},
  timestamp = {Mon, 13 Aug 2018 16:47:23 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1807-05174},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{gunther2019mechanization,
  author    = {Emmanuel Gunther and
               Miguel Pagano and
               Pedro S{\'{a}}nchez Terraf},
  title     = {Mechanization of Separation in Generic Extensions},
  journal   = {CoRR},
  volume    = {abs/1901.03313},
  year      = {2019},
  url       = {http://arxiv.org/abs/1901.03313},
  archivePrefix = {arXiv},
  eprint    = {1901.03313},
  timestamp = {Fri, 01 Feb 2019 13:39:59 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1901-03313},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{scott2014stochastic,
  title={Stochastic $\lambda$-calculi},
  author={Scott, Dana},
  journal={Journal of Applied Logic},
  volume={12},
  number={3},
  pages={369--376},
  year={2014},
  publisher={Elsevier}
}

@inproceedings{bacci2018boolean,
  title={Boolean-valued semantics for the stochastic $\lambda$-calculus},
  author={Bacci, Giorgio and Furber, Robert and Kozen, Dexter and Mardare, Radu and Panangaden, Prakash and Scott, Dana},
  booktitle={Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
  pages={669--678},
  year={2018},
  organization={ACM}
}

@article{scott2008algebraic,
  title={The Algebraic Intepretation of Quantifiers: intuitionistic and classical},
  author={Scott, Dana},
  journal={Andrzej Mostowski and Foundational Studies},
  pages={289--312},
  year={2008},
  publisher={IOS Press Amsterdam}
}

@article{kanamori1996mathematical,
  title={The mathematical development of set theory from {Cantor} to {Cohen}},
  author={Kanamori, Akihiro},
  journal={Bulletin of Symbolic Logic},
  volume={2},
  number={1},
  pages={1--71},
  year={1996},
  publisher={Cambridge University Press}
}

@book{kanamori2008higher,
  title={The Higher Infinite: Large Cardinals in Set Theory from their beginnings},
  author={Kanamori, Akihiro},
  year={2008},
  publisher={Springer Science \& Business Media}
}

@article{hamkins2012well,
  title={Well-founded Boolean ultrapowers as large cardinal embeddings},
  author={Hamkins, Joel David and Seabold, Daniel Evan},
  journal={arXiv preprint arXiv:1206.6075},
  year={2012}
}

@article{moore2019method,
  title={The method of forcing},
  author={Moore, Justin Tatch},
  journal={arXiv preprint arXiv:1902.03235},
  year={2019}
}

@book {kunen2014set,
    AUTHOR = {Kunen, Kenneth},
     TITLE = {Set theory},
    SERIES = {Studies in Logic and the Foundations of Mathematics},
    VOLUME = {102},
 PUBLISHER = {North-Holland Publishing Co., Amsterdam-New York},
      YEAR = {1980},
     PAGES = {xvi+313},
      ISBN = {0-444-85401-0},
   MRCLASS = {03-02 (03E35 03Exx 04-02)},
  MRNUMBER = {597342},
MRREVIEWER = {U. Felgner},
}

@article{scott1967proof,
  title={A Proof of the Independence of the Continuum Hypothesis},
  author={Scott, Dana},
  journal={Theory of Computing Systems},
  volume={1},
  number={2},
  pages={89--111},
  year={1967},
  publisher={Springer}
}

@book{givant2008introduction,
  title={Introduction to Boolean algebras},
  author={Givant, Steven and Halmos, Paul},
  year={2008},
  publisher={Springer Science \& Business Media}
}

@inproceedings{werner1997sets,
  title={Sets in types, types in sets},
  author={Werner, Benjamin},
  booktitle={International Symposium on Theoretical Aspects of Computer Software},
  pages={530--546},
  year={1997},
  organization={Springer}
}

@misc{sebastian1,
 title={Lean 4: A Guided Preview},
 author={Ullrich, Sebastian},
 howpublished={\url{https://leanprover.github.io/talks/vu2019.pdf}},
 urldate = {2019-01-04},
 note = {Slides}
}

@book{bell2011set,
  title={Set theory: Boolean-valued models and independence proofs},
  author={Bell, John L},
  volume={47},
  year={2011},
  publisher={Oxford University Press}
}

@unpublished{mario1,
  title={The type theory of {Lean}},
  author={Carneiro, Mario},
  year={2019},
  note={In preparation (\url{https://github.com/digama0/lean-type-theory/releases})}
  }

@book{manin2009course,
  title={A course in mathematical logic for mathematicians},
  author={Manin, Yu I},
  volume={53},
  year={2009},
  publisher={Springer Science \& Business Media}
}

@book{jech2013set,
  title={Set theory},
  author={Jech, Thomas},
  year={2013},
  publisher={Springer Science \& Business Media}
}

@article{cantor1878beitrag,
  title={Ein {Beitrag} zur {Mannigfaltigkeitslehre}},
  author={Cantor, Georg},
  journal={Journal f\"{u}r die reine und angewandte Mathematik},
  volume={84},
  pages={242--258},
  year={1878}
}

@article{cohen1964independence2,
  title={The independence of the continuum hypothesis, {II}},
  author={Cohen, Paul J},
  journal={Proceedings of the National Academy of Sciences},
  volume={51},
  number={1},
  pages={105},
  year={1964},
  publisher={National Academy of Sciences}
}

@unpublished{scott-solovay,
  title={Boolean algebras and forcing},
  year={1967},
  author={Scott, Dana and Solovay, Robert},
  note={Unpublished manuscript}
}

@inproceedings{aczel1978type,
  title={The type theoretic interpretation of constructive set theory},
  author={Aczel, Peter},
  booktitle={Logic Colloquium},
  volume={77},
  pages={55--66},
  year={1978}
}

@incollection{aczel1986type,
  title={The type theoretic interpretation of constructive set theory: inductive definitions},
  author={Aczel, Peter},
  booktitle={Studies in Logic and the Foundations of Mathematics},
  volume={114},
  pages={17--49},
  year={1986},
  publisher={Elsevier}
}

@incollection{aczel1982type,
  title={The type theoretic interpretation of constructive set theory: choice principles},
  author={Aczel, Peter},
  booktitle={Studies in Logic and the Foundations of Mathematics},
  volume={110},
  pages={1--40},
  year={1982},
  publisher={Elsevier}
}

@misc{mario2,
  title={Natural deduction in the {Metamath} Proof Explorer},
  author={Mario Carneiro},
  year = {2014},
  howpublished = {\url{http://us.metamath.org/mpeuni/mmnatded.html}},
  note = {Slides (\url{http://us.metamath.org/ocat/natded.pdf})}
}

@article{paulson1996mechanizing,
  author    = {Lawrence C. Paulson and
               Krzysztof Grabczewski},
  title     = {Mechanizing Set Theory},
  journal   = {J. Autom. Reasoning},
  volume    = {17},
  number    = {3},
  pages     = {291--323},
  year      = {1996},
  url       = {https://doi.org/10.1007/BF00283132},
  doi       = {10.1007/BF00283132},
  timestamp = {Sat, 20 May 2017 00:22:31 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/jar/PaulsonG96},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{paulson1993set,
  author    = {Lawrence C. Paulson},
  title     = {{Set Theory for Verification: I.} {From} Foundations to Functions},
  journal   = {J. Autom. Reasoning},
  volume    = {11},
  number    = {3},
  pages     = {353--389},
  year      = {1993},
  url       = {https://doi.org/10.1007/BF00881873},
  doi       = {10.1007/BF00881873},
  timestamp = {Wed, 14 Nov 2018 10:38:36 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/jar/Paulson93},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{paulson2002reflection,
  author    = {Lawrence C. Paulson},
  title     = {The Reflection Theorem: {A} Study in Meta-theoretic Reasoning},
  booktitle = {Automated Deduction - CADE-18, 18th International Conference on Automated
               Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings},
  pages     = {377--391},
  year      = {2002},
  crossref  = {DBLP:conf/cade/2002},
  url       = {https://doi.org/10.1007/3-540-45620-1\_31},
  doi       = {10.1007/3-540-45620-1\_31},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/Paulson02},
  bibsource = {dblp computer science bibliography, https://dblp.org}
} 

@proceedings{DBLP:conf/cade/2002,
  editor    = {Andrei Voronkov},
  title     = {Automated Deduction - CADE-18, 18th International Conference on Automated
               Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2392},
  publisher = {Springer},
  year      = {2002},
  url       = {https://doi.org/10.1007/3-540-45620-1},
  doi       = {10.1007/3-540-45620-1},
  isbn      = {3-540-43931-5},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2002},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{Hudon2015TheUM,
  title={The {Unit-B} method: refinement guided by progress concerns},
  author={Simon Hudon and Thai Son Hoang and Jonathan S. Ostroff},
  journal={Software \& Systems Modeling},
  year={2015},
  volume={15},
  pages={1091-1116}
}

@misc{unitb,
  title={Temporal logic in {Unit-B}},
  author={Simon Hudon},
  note={\url{https://github.com/unitb/temporal-logic}},
  year={2018}
}