{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:06Z","timestamp":1750219806231,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T00:00:00Z","timestamp":1673395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100018694","name":"HORIZON EUROPE Marie Sklodowska-Curie Actions","doi-asserted-by":"publisher","award":["101024493"],"award-info":[{"award-number":["101024493"]}],"id":[{"id":"10.13039\/100018694","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575690","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"159-166","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Computational Cantor-Bernstein and Myhill\u2019s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)"],"prefix":"10.1145","author":[{"given":"Yannick","family":"Forster","sequence":"first","affiliation":[{"name":"Inria, France \/ Saarland University, Germany"}]},{"given":"Felix","family":"Jahn","sequence":"additional","affiliation":[{"name":"Saarland University, Germany"}]},{"given":"Gert","family":"Smolka","sequence":"additional","affiliation":[{"name":"Saarland University, Germany"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/bf01457734"},{"key":"e_1_3_2_1_2_1","volume-title":"Zeitschrift f\u00fcr Philosophie und philosophische Kritik 91","author":"Cantor Georg","year":"1887","unstructured":"Georg Cantor. Mitteilungen zur Lehre vom Transfiniten. In Zeitschrift f\u00fcr Philosophie und philosophische Kritik 91, 1887."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02124929"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s40062-021-00284-6"},{"key":"e_1_3_2_1_5_1","volume-title":"Challenge: how much beyond finite sets with decidable equality can CSB apply to in constructive mathematics?","author":"Mart\u00edn H\u00f6tzel","year":"2022","unstructured":"Mart\u00edn H\u00f6tzel Escard\u00f3 (@EscardoMartin). \u201cChallenge: how much beyond finite sets with decidable equality can CSB apply to in constructive mathematics?\u201d 12:47 PM - 3 Feb 2022. Tweet. https:\/\/web.archive.org\/web\/20220203205238\/https:\/\/twitter.com\/EscardoMartin\/status\/1489339787005906958, 2022. Accessed: (September 14th)."},{"key":"e_1_3_2_1_7_1","volume-title":"31st EACSL Annual Conference on Computer Science Logic (CSL 2023","author":"Forster Yannick","year":"2023","unstructured":"Yannick Forster and Felix Jahn. Constructive and Synthetic Reducibility Degrees: Post\u2019s Problem for Many-one and Truth-table Reducibility in Coq. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), Dagstuhl, Germany. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2023.16 doi:10.4230\/LIPIcs.CSL.2023.16."},{"key":"e_1_3_2_1_8_1","volume-title":"February","author":"Forster Yannick","year":"2022","unstructured":"Yannick Forster, Felix Jahn, and Gert Smolka. A Constructive and Synthetic Theory of Reducibility: Myhill\u2019s Isomorphism Theorem and Post\u2019s Problem for Many-one and Truth-table Reducibility in Coq (Full Version). preprint, February 2022. URL: https:\/\/hal.inria.fr\/hal-03580081."},{"key":"e_1_3_2_1_9_1","volume-title":"Bachelor\u2019s thesis","author":"Jahn Felix","year":"2020","unstructured":"Felix Jahn. Synthetic One-One, Many-One, and Truth-Table Reducibility in Coq. Bachelor\u2019s thesis, Saarland University, 2020. URL: https:\/\/ps.uni-saarland.de\/~jahn\/bachelor.php."},{"key":"e_1_3_2_1_10_1","first-page":"12","volume-title":"13th International Conference on Interactive Theorem Proving (ITP 2022), volume 237 of Leibniz International Proceedings in Informatics (LIPIcs)","author":"Kirst Dominik","year":"2022","unstructured":"Dominik Kirst. Computational Back-And-Forth Arguments in Constructive Type Theory. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022), volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1\u201322:12, Dagstuhl, Germany, 2022. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik. URL: https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2022\/16731, https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.22 doi:10.4230\/LIPIcs.ITP.2022.22."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/bf01461161"},{"key":"e_1_3_2_1_12_1","volume-title":"Sur la th\u00e9orie des ensembles. Comptes Rendus Hebdomadaires des S\u00e9ances de l\u2019Acad\u00e9mie des Sciences, 143:110\u2013112","author":"Gyula Jules K\u00f6nig","year":"1906","unstructured":"Jules K\u00f6nig (Gyula K\u0151nig). Sur la th\u00e9orie des ensembles. Comptes Rendus Hebdomadaires des S\u00e9ances de l\u2019Acad\u00e9mie des Sciences, 143:110\u2013112, 1906. URL: https:\/\/gallica.bnf.fr\/ark:\/12148\/bpt6k30977.image.f110.langEN."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19550010205"},{"key":"e_1_3_2_1_14_1","volume-title":"Cantor-Bernstein implies excluded middle. CoRR, abs\/1904.09193","author":"Pradic Pierre","year":"2019","unstructured":"Pierre Pradic and Chad E. Brown. Cantor-Bernstein implies excluded middle. CoRR, abs\/1904.09193, 2019. http:\/\/arxiv.org\/abs\/1904.09193 arXiv:1904.09193."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/28907"},{"key":"e_1_3_2_1_16_1","first-page":"81","volume":"5","author":"Schr\u00f6der Ernst","year":"1896","unstructured":"Ernst Schr\u00f6der. \u00dcber G. Cantorsche Satze. Jahresberichtder Deutsche Mathematiker-Vereinigung, 5:81\u201382, 1896.","journal-title":"Cantorsche Satze. Jahresberichtder Deutsche Mathematiker-Vereinigung"},{"issue":"1","key":"e_1_3_2_1_17_1","first-page":"74","article-title":"Who invented cantor\u2019s back-and-forth argument?","volume":"4","author":"Silver Charles L","year":"1994","unstructured":"Charles L Silver. Who invented cantor\u2019s back-and-forth argument? Modern Logic, 4(1):74\u201378, 1994.","journal-title":"Modern Logic"},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of the ACM on Programming Languages, 3(ICFP):1\u201329","author":"Sozeau Matthieu","year":"2019","unstructured":"Matthieu Sozeau and Cyprien Mangin. Equations reloaded: High-level dependently-typed functional programming and proving in coq. Proceedings of the ACM on Programming Languages, 3(ICFP):1\u201329, 2019. https:\/\/doi.org\/10.1145\/3341690 doi:10.1145\/3341690."},{"key":"e_1_3_2_1_19_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book","author":"Foundations Program The Univalent","year":"2013","unstructured":"The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study, 2013."},{"key":"e_1_3_2_1_20_1","volume-title":"Schr\u00f6der\u2013Bernstein theorem \u2014 Wikipedia, the free encyclopedia. https:\/\/en.wikipedia.org\/w\/index.php?title=Schr","author":"Wikipedia","year":"2022","unstructured":"Wikipedia contributors. Schr\u00f6der\u2013Bernstein theorem \u2014 Wikipedia, the free encyclopedia. https:\/\/en.wikipedia.org\/w\/index.php?title=Schr 2022. [Online; accessed 14-September-2022]."}],"event":{"name":"CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Boston MA USA","acronym":"CPP '23"},"container-title":["Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575690","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575690","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:38Z","timestamp":1750178738000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575690"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":19,"alternative-id":["10.1145\/3573105.3575690","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575690","relation":{},"subject":[],"published":{"date-parts":[[2023,1,11]]},"assertion":[{"value":"2023-01-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}