Quelle  root.bib

@article{DBLP:journals/jar/PaulsonG96,
  author    = {Lawrence C. Paulson and
               Krzysztof Grabczewski},
  title     = {Mechanizing Set Theory},
  journal   = {J. Autom. Reasoning},
  volume    = {17},
  number    = {3},
  pages     = {291--323},
  year      = {1996},
  xurl       = {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}
}

@inproceedings{2018arXiv180705174G,
       author = {Gunther, Emmanuel and Pagano, Miguel and S{\'a}nchez Terraf, Pedro},
  title     = {First Steps Towards a Formalization of Forcing},
  booktitle = {Proceedings of the 13th Workshop on Logical and Semantic Frameworks
               with Applications, {LSFA} 2018, Fortaleza, Brazil, September 26-28,
               2018},
  pages     = {119--136},
  year      = {2018},
  url       = {https://doi.org/10.1016/j.entcs.2019.07.008},
  doi       = {10.1016/j.entcs.2019.07.008},
  timestamp = {Wed, 05 Feb 2020 13:47:23 +0100},
  biburl    = {https://dblp.org/rec/journals/entcs/GuntherPT19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}


@ARTICLE{2019arXiv190103313G,
       author = {Gunther, Emmanuel and Pagano, Miguel and S{\'a}nchez Terraf, Pedro},
        title = "{Mechanization of Separation in Generic Extensions}",
      journal = {arXiv e-prints},
     keywords = {Computer Science - Logic in Computer Science, Mathematics - Logic, 03B35 (Primary) 03E40, 03B70, 68T15 (Secondary), F.4.1},
         year = 2019,
        month = Jan,
          eid = {arXiv:1901.03313},
       volume = {1901.03313},
archivePrefix = {arXiv},
       eprint = {1901.03313},
 primaryClass = {cs.LO},
       adsurl = {https://ui.adsabs.harvard.edu/\#abs/2019arXiv190103313G},
      adsnote = {Provided by the SAO/NASA Astrophysics Data System},
     abstract = {We mechanize, in the proof assistant Isabelle, a proof of the axiom-scheme of Separation in generic extensions of models of set theory by using the fundamental theorems of forcing. We also formalize the satisfaction of the axioms of Extensionality, Foundation, Union, and Powerset. The axiom of Infinity is likewise treated, under additional assumptions on the ground model. In order to achieve these goals, we extended Paulson's library on constructibility with renaming of variables for internalized formulas, improved results on definitions by recursion on well-founded relations, and sharpened hypotheses in his development of relativization and absoluteness.}
}

@ARTICLE{2020arXiv200109715G,
       author = {{Gunther}, Emmanuel and {Pagano}, Miguel and {S{\'a}nchez Terraf}, Pedro},
        title = "{Formalization of Forcing in Isabelle/ZF}",
      journal = {arXiv e-prints},
     keywords = {Computer Science - Logic in Computer Science, Mathematics - Logic},
         year = 2020,
        month = jan,
          eid = {arXiv:2001.09715},
       volume = {2001.09715},
archivePrefix = {arXiv},
       eprint = {2001.09715},
 primaryClass = {cs.LO},
       adsurl = {https://ui.adsabs.harvard.edu/abs/2020arXiv200109715G},
      adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}