{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:46:07Z","timestamp":1759146367045,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,1,20]],"date-time":"2020-01-20T00:00:00Z","timestamp":1579478400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Alfred P. Sloan Foundation","award":["G-2018-10067"],"award-info":[{"award-number":["G-2018-10067"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,1,20]]},"DOI":"10.1145\/3372885.3373826","type":"proceedings-article","created":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T13:09:33Z","timestamp":1579698573000},"page":"353-366","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["A formal proof of the independence of the continuum hypothesis"],"prefix":"10.1145","author":[{"given":"Jesse Michael","family":"Han","sequence":"first","affiliation":[{"name":"University of Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Floris","family":"van Doorn","sequence":"additional","affiliation":[{"name":"University of Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,1,22]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"55","article-title":"The type theoretic interpretation of constructive set theory","volume":"77","author":"Aczel Peter","year":"1978","journal-title":"Logic Colloquium"},{"volume-title":"Studies in Logic and the Foundations of Mathematics.","author":"Aczel Peter","key":"e_1_3_2_1_2_1"},{"volume-title":"Studies in Logic and the Foundations of Mathematics.","author":"Aczel Peter","key":"e_1_3_2_1_3_1"},{"key":"e_1_3_2_1_4_1","unstructured":"John L Bell. 2011. Set theory: Boolean-valued models and independence proofs. Vol. 47. Oxford University Press.  John L Bell. 2011. Set theory: Boolean-valued models and independence proofs. Vol. 47. Oxford University Press."},{"key":"e_1_3_2_1_5_1","unstructured":"Stefan Berghofer. 2007. First-Order Logic According to Fitting. Archive of Formal Proofs (Aug. 2007). http:\/\/isa-afp.org\/entries\/FOL-Fitting. html Formal proof development.  Stefan Berghofer. 2007. First-Order Logic According to Fitting. Archive of Formal Proofs (Aug. 2007). http:\/\/isa-afp.org\/entries\/FOL-Fitting. html Formal proof development."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1515\/crll.1878.84.242"},{"key":"e_1_3_2_1_7_1","unstructured":"Mario Carneiro. 2019. The type theory of Lean. (2019). In preparation ( https:\/\/github.com\/digama0\/lean-type-theory\/releases ).  Mario Carneiro. 2019. The type theory of Lean. (2019). In preparation ( https:\/\/github.com\/digama0\/lean-type-theory\/releases )."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.50.6.1143"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.51.1.105"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(70)90012-4"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Steven Givant and Paul Halmos. 2008. Introduction to Boolean algebras. Springer Science & Business Media.  Steven Givant and Paul Halmos. 2008. Introduction to Boolean algebras. Springer Science & Business Media.","DOI":"10.1007\/978-0-387-68436-9_2"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.24.12.556"},{"key":"e_1_3_2_1_15_1","unstructured":"Emmanuel Gunther Miguel Pagano and Pedro S\u00e1nchez Terraf. 2018. First steps towards a formalization of Forcing. CoRR abs\/1807.05174 (2018). arXiv: 1807.05174 http:\/\/arxiv.org\/abs\/1807.05174  Emmanuel Gunther Miguel Pagano and Pedro S\u00e1nchez Terraf. 2018. First steps towards a formalization of Forcing. CoRR abs\/1807.05174 (2018). arXiv: 1807.05174 http:\/\/arxiv.org\/abs\/1807.05174"},{"key":"e_1_3_2_1_16_1","unstructured":"Emmanuel Gunther Miguel Pagano and Pedro S\u00e1nchez Terraf. 2019. Mechanization of Separation in Generic Extensions. CoRR abs\/1901.03313 (2019). arXiv: 1901.03313 http:\/\/arxiv.org\/abs\/1901. 03313  Emmanuel Gunther Miguel Pagano and Pedro S\u00e1nchez Terraf. 2019. Mechanization of Separation in Generic Extensions. CoRR abs\/1901.03313 (2019). arXiv: 1901.03313 http:\/\/arxiv.org\/abs\/1901. 03313"},{"key":"e_1_3_2_1_17_1","unstructured":"Joel David Hamkins and Daniel Evan Seabold. 2012. Well-founded Boolean ultrapowers as large cardinal embeddings. arXiv preprint arXiv:1206.6075 (2012).  Joel David Hamkins and Daniel Evan Seabold. 2012. Well-founded Boolean ultrapowers as large cardinal embeddings. arXiv preprint arXiv:1206.6075 (2012)."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.19"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055135"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"John Harrison. 2009. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press.  John Harrison. 2009. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press.","DOI":"10.1017\/CBO9780511576430"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01458215"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Simon Hudon Thai Son Hoang and Jonathan S. Ostroff. 2015. The Unit-B method: refinement guided by progress concerns. Software & Systems Modeling 15 (2015) 1091\u20131116.  Simon Hudon Thai Son Hoang and Jonathan S. Ostroff. 2015. The Unit-B method: refinement guided by progress concerns. Software & Systems Modeling 15 (2015) 1091\u20131116.","DOI":"10.1007\/s10270-015-0456-2"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868"},{"key":"e_1_3_2_1_24_1","unstructured":"Danko Ilik. 2010. Constructive completeness proofs and delimited control. Ph.D. Dissertation. Ecole Polytechnique X.  Danko Ilik. 2010. Constructive completeness proofs and delimited control. Ph.D. Dissertation. Ecole Polytechnique X."},{"key":"e_1_3_2_1_25_1","unstructured":"Thomas Jech. 2013. Set theory. Springer Science & Business Media.  Thomas Jech. 2013. Set theory. Springer Science & Business Media."},{"key":"e_1_3_2_1_26_1","volume-title":"Studies in Logic and the Foundations of Mathematics","volume":"102","author":"Kunen Kenneth","year":"1980"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Yu I Manin. 2009. A course in mathematical logic for mathematicians. Vol. 53. Springer Science & Business Media.  Yu I Manin. 2009. A course in mathematical logic for mathematicians. Vol. 53. Springer Science & Business Media.","DOI":"10.1007\/978-1-4419-0615-1"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(70)90009-4"},{"key":"e_1_3_2_1_29_1","unstructured":"The mathlib Community. 2019. The Lean mathematical library. arXiv e-prints Article arXiv:1910.09336 (Oct 2019) arXiv:1910.09336 pages. arXiv: cs.LO\/1910.09336  The mathlib Community. 2019. The Lean mathematical library. arXiv e-prints Article arXiv:1910.09336 (Oct 2019) arXiv:1910.09336 pages. arXiv: cs.LO\/1910.09336"},{"key":"e_1_3_2_1_30_1","unstructured":"Justin Tatch Moore. 2019. The method of forcing. arXiv preprint arXiv:1902.03235 (2019).  Justin Tatch Moore. 2019. The method of forcing. arXiv preprint arXiv:1902.03235 (2019)."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_16"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881873"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45620-1_31"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_52"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00283132"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_19"},{"key":"e_1_3_2_1_37_1","unstructured":"Anders Schlichtkrull. 2018. Formalization of logic in the Isabelle proof assistant. Ph.D. Dissertation. Technical University of Denmark.  Anders Schlichtkrull. 2018. Formalization of logic in the Isabelle proof assistant. Ph.D. Dissertation. Technical University of Denmark."},{"key":"e_1_3_2_1_38_1","first-page":"89","article-title":"A Proof of the Independence of the Continuum Hypothesis","volume":"1","author":"Scott Dana","year":"1967","journal-title":"Theory of Computing Systems"},{"key":"e_1_3_2_1_39_1","unstructured":"Dana Scott. 2008. The Algebraic Intepretation of Quantifiers: intuitionistic and classical. Andrzej Mostowski and Foundational Studies (2008) 289\u2013312.  Dana Scott. 2008. The Algebraic Intepretation of Quantifiers: intuitionistic and classical. Andrzej Mostowski and Foundational Studies (2008) 289\u2013312."},{"key":"e_1_3_2_1_40_1","unstructured":"Dana Scott and Robert Solovay. 1967. Boolean algebras and forcing. (1967). Unpublished manuscript.  Dana Scott and Robert Solovay. 1967. Boolean algebras and forcing. (1967). Unpublished manuscript."},{"key":"e_1_3_2_1_41_1","unstructured":"Natarajan Shankar. 1997. Metamathematics machines and G\u00f6del\u2019s proof. Vol. 38. Cambridge University Press.  Natarajan Shankar. 1997. Metamathematics machines and G\u00f6del\u2019s proof. Vol. 38. Cambridge University Press."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02757281"},{"volume-title":"Axiomatic set theory","author":"Shoenfield Joseph R","key":"e_1_3_2_1_43_1"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Sebastian Ullrich and Leonardo de Moura. 2019. Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming. arXiv: cs.PL\/1908.05647  Sebastian Ullrich and Leonardo de Moura. 2019. Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming. arXiv: cs.PL\/1908.05647","DOI":"10.1145\/3412932.3412935"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Nik Weaver. 2014. Forcing for mathematicians. World Scientific.  Nik Weaver. 2014. Forcing for mathematicians. World Scientific.","DOI":"10.1142\/8962"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014566"}],"event":{"name":"POPL '20: 47th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"New Orleans LA USA","acronym":"POPL '20"},"container-title":["Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373826","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372885.3373826","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:09Z","timestamp":1750200069000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373826"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,20]]},"references-count":46,"alternative-id":["10.1145\/3372885.3373826","10.1145\/3372885"],"URL":"https:\/\/doi.org\/10.1145\/3372885.3373826","relation":{},"subject":[],"published":{"date-parts":[[2020,1,20]]},"assertion":[{"value":"2020-01-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}