{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:14:23Z","timestamp":1759637663365,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,1,14]],"date-time":"2019-01-14T00:00:00Z","timestamp":1547424000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,1,14]]},"DOI":"10.1145\/3293880.3294091","type":"proceedings-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:56Z","timestamp":1546608836000},"page":"38-51","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["On synthetic undecidability in Coq, with an application to the Entscheidungsproblem"],"prefix":"10.1145","author":[{"given":"Yannick","family":"Forster","sequence":"first","affiliation":[{"name":"Saarland University, Germany"}]},{"given":"Dominik","family":"Kirst","sequence":"additional","affiliation":[{"name":"Saarland University, Germany"}]},{"given":"Gert","family":"Smolka","sequence":"additional","affiliation":[{"name":"Saarland University, Germany"}]}],"member":"320","published-online":{"date-parts":[[2019,1,14]]},"reference":[{"unstructured":"Thomas Arts and W Dekkers. 1992. Embedding first order predicate logic in second order propositional logic. Master's thesis University of Njimegen (1992). Thomas Arts and W Dekkers. 1992. Embedding first order predicate logic in second order propositional logic. Master's thesis University of Njimegen (1992).","key":"e_1_3_2_1_1_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_2_1","DOI":"10.1016\/j.entcs.2005.11.049"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1515\/tmj-2017-0107"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_4_1","DOI":"10.1016\/j.apal.2004.01.002"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_5_1","DOI":"10.1016\/S0168-0072(01)00073-2"},{"doi-asserted-by":"crossref","unstructured":"E. Boerger E. Gr\u00e4del and Y. Gurevich. 1997. The classical decision problem. Springer. E. Boerger E. Gr\u00e4del and Y. Gurevich. 1997. The classical decision problem . Springer.","key":"e_1_3_2_1_6_1","DOI":"10.1007\/978-3-642-59207-2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.1145\/1411203.1411226"},{"doi-asserted-by":"crossref","unstructured":"Alonzo Church. 1936. A note on the Entscheidungsproblem. The journal of symbolic logic 1 1 (1936) 40-41. Alonzo Church. 1936. A note on the Entscheidungsproblem. The journal of symbolic logic 1 1 (1936) 40-41.","key":"e_1_3_2_1_8_1","DOI":"10.2307\/2269326"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_9_1","DOI":"10.1016\/j.scico.2016.02.004"},{"unstructured":"Thierry Coquand and Bassel Mannaa. 2016. The independence of Markov's principle in type theory. arXiv preprint arXiv:1602.04530 (2016). Thierry Coquand and Bassel Mannaa. 2016. The independence of Markov's principle in type theory. arXiv preprint arXiv:1602.04530 (2016).","key":"e_1_3_2_1_10_1"},{"unstructured":"Hilbert David and Ackermann Wilhelm. 1928. Grundz\u00fcge der theoretischen Logik. (1928). Hilbert David and Ackermann Wilhelm. 1928. Grundz\u00fcge der theoretischen Logik. (1928).","key":"e_1_3_2_1_11_1"},{"volume-title":"ITP 2018 (Lecture Notes in Computer Science)","author":"Forster Yannick","key":"e_1_3_2_1_12_1"},{"volume-title":"Coq Workshop 2016","year":"2016","author":"Forster Yannick","key":"e_1_3_2_1_13_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_14_1","DOI":"10.1145\/3293880.3294096"},{"volume-title":"ITP","year":"2017","author":"Forster Yannick","key":"e_1_3_2_1_15_1"},{"volume-title":"Higher set theory","author":"Friedman Harvey","key":"e_1_3_2_1_16_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_17_1","DOI":"10.1007\/BF01565428"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_18_1","DOI":"10.1007\/BF01696781"},{"unstructured":"Kurt G\u00f6del. 1933. Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse eines mathematischen Kolloquiums 4 1933 (1933) 34-38. Kurt G\u00f6del. 1933. Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse eines mathematischen Kolloquiums 4 1933 (1933) 34-38.","key":"e_1_3_2_1_19_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_20_1","DOI":"10.1109\/LICS.2010.49"},{"unstructured":"Hugo Herbelin and Danko Ilik. 2016. An analysis of the constructive content of Henkin's proof of G\u00f6del's completeness theorem. (2016). Hugo Herbelin and Danko Ilik. 2016. An analysis of the constructive content of Henkin's proof of G\u00f6del's completeness theorem. (2016).","key":"e_1_3_2_1_21_1"},{"key":"e_1_3_2_1_22_1","first-page":"1521","article-title":"Formalizing the meta-theory of first-order predicate logic","volume":"54","author":"Herbelin Hugo","year":"2017","journal-title":"Journal of the korean Mathematical society"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1007\/978-3-642-02261-6_17"},{"unstructured":"Hugo Herbelin and Gyesik Lee. 2014. Formalizing Logical Meta-theory - Semantical Cut-Elimination using Kripke Models for first-order Predicate Logic. (2014). Hugo Herbelin and Gyesik Lee. 2014. Formalizing Logical Meta-theory - Semantical Cut-Elimination using Kripke Models for first-order Predicate Logic. (2014).","key":"e_1_3_2_1_24_1"},{"volume-title":"The LEJ Brouwer centenary symposium","author":"Hyland J Martin E","key":"e_1_3_2_1_25_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_26_1","DOI":"10.1007\/s10817-018-9480-6"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_27_1","DOI":"10.2178\/bsl\/1122038996"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_28_1","DOI":"10.2307\/2964291"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_29_1","DOI":"10.2307\/421172"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_30_1","DOI":"10.2307\/2272390"},{"unstructured":"Zohar Manna. 2003. Mathematical theory of computation. Dover Publications Incorporated. Zohar Manna. 2003. Mathematical theory of computation . Dover Publications Incorporated.","key":"e_1_3_2_1_31_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_32_1","DOI":"10.5555\/2033939.2033963"},{"unstructured":"Russell SS O'Connor. 2009. Incompleteness & completeness: formalizing logic and analysis in type theory. PhD thesis Radboud University of Njimegen (2009). Russell SS O'Connor. 2009. Incompleteness & completeness: formalizing logic and analysis in type theory. PhD thesis Radboud University of Njimegen (2009).","key":"e_1_3_2_1_33_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_34_1","DOI":"10.1090\/S0002-9904-1946-08555-9"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_35_1","DOI":"10.1007\/978-3-662-57669-4_11"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_36_1","DOI":"10.2307\/2273473"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_37_1","DOI":"10.1007\/978-3-319-22102-1_24"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_38_1","DOI":"10.1305\/ndjfl\/1093891803"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_39_1","DOI":"10.1016\/j.apal.2012.05.009"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_40_1","DOI":"10.1215\/00294527-2010-029"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_41_1","DOI":"10.1017\/S0960129511000119"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_42_1","DOI":"10.1016\/0747-7171(92)90016-W"},{"unstructured":"A.S. Troelstra and D. Van Dalen. 1988. Constructivism in Mathematics. North-Holland Amsterdam. A.S. Troelstra and D. Van Dalen. 1988. Constructivism in Mathematics . North-Holland Amsterdam.","key":"e_1_3_2_1_43_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_44_1","DOI":"10.1112\/plms\/s2-42.1.230"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_45_1","DOI":"10.5555\/645893.671612"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"crossref","first-page":"159","DOI":"10.2307\/2272955","article-title":"An intuitionistic completeness theorem for intuitionistic predicate logic","volume":"41","author":"Veldman Wim","year":"1976","journal-title":"The Journal of Symbolic Logic"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_47_1","DOI":"10.1007\/978-3-642-39634-2_13"}],"event":{"sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"acronym":"CPP '19","name":"CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Cascais Portugal"},"container-title":["Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294091","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293880.3294091","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:49Z","timestamp":1750207429000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294091"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,14]]},"references-count":47,"alternative-id":["10.1145\/3293880.3294091","10.1145\/3293880"],"URL":"https:\/\/doi.org\/10.1145\/3293880.3294091","relation":{},"subject":[],"published":{"date-parts":[[2019,1,14]]},"assertion":[{"value":"2019-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}