@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{2020arXiv200109715G,
       author = {Gunther, Emmanuel and Pagano, Miguel and S{\'a}nchez Terraf, Pedro},
        title = "{Formalization of Forcing in Isabelle/ZF}",
    isbn      = {978-3-662-45488-6},
    booktitle = {Automated Reasoning. 10th International Joint Conference, IJCAR 2020, Paris, France, July 1--4, 2020, Proceedings, Part II},
    volume    = 12167,
    series    = {Lecture Notes in Artificial Intelligence},
    editor    = {Peltier, Nicolas and  Sofronie-Stokkermans, Viorica},
    publisher = {Springer International Publishing},
    doi       = {10.1007/978-3-030-51054-1},
    pages     = {221--235},
     keywords = {Computer Science - Logic in Computer Science, Mathematics - Logic, 03B35 (Primary) 03E40, 03B70, 68T15 (Secondary), F.4.1},
         year = 2020,
          eid = {arXiv:2001.09715},
archivePrefix = {arXiv},
       eprint = {2001.09715},
 primaryClass = {cs.LO},
       adsurl = {https://ui.adsabs.harvard.edu/abs/2020arXiv200109715G},
     abstract = {We formalize the theory of forcing in the set theory framework of
Isabelle/ZF. Under the assumption of the existence of a countable
transitive model of $\mathit{ZFC}$, we construct a proper generic extension and show
that the latter also satisfies $\mathit{ZFC}$. In doing so, we remodularized
Paulson's ZF-Constructibility library.},
      adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

@Book{Jech_Millennium,
    author =	"Thomas Jech",
    title =	"Set Theory. The Millennium Edition",
    series =	"Springer Monographs in Mathematics",
    publisher = "Springer-Verlag",
    edition = "Third",
    year =	"2002",
    note = {Corrected fourth printing, 2006}
}

@misc{apunte_st,
  author = {S{\'a}nchez Terraf, Pedro},
  title = "Course notes on set theory",
  howpublished = {online},
  year = 2019,
  note = "In Spanish",
  url = {https://cs.famaf.unc.edu.ar/~pedro/home_en.html#set_theory}
}

@book{kunen2011set,
  title={Set Theory},
  author={Kunen, K.},
  edition = {Second},
  isbn=9781848900509,
  series={Studies in Logic},
  url={https://books.google.com.ar/books?id=Zn8ppwAACAAJ},
  year=2011,
  publisher={College Publications},
  note = {Revised edition, 2013}
}

@Book{JW,
    author =	"Winfried Just and Martin Weese",
    title =	"Discovering Modern Set Theory. II",
    series =	"Grad. Studies in Mathematics",
    volume =	"18",
    publisher = "American Mathematical Society", 
    year =	"1997"
}

@article{Transitive_Models-AFP,
  author  = {Emmanuel Gunther and Miguel Pagano and Sánchez Terraf, Pedro and Matías Steinberg},
  title   = {Transitive Models of Fragments of {ZFC}},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2022,
  note    = {\url{https://isa-afp.org/entries/Transitive_Models.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{Independence_CH-AFP,
  author  = {Emmanuel Gunther and Miguel Pagano and Sánchez Terraf, Pedro and Matías Steinberg},
  title   = {The Independence of the Continuum Hypothesis in {Isabelle/ZF}},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2022,
  note    = {\url{https://isa-afp.org/entries/Independence_CH.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
