{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:30:40Z","timestamp":1750221040523,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":39,"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"}],"funder":[{"DOI":"10.13039\/501100005304","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["16-CE91-0002"],"award-info":[{"award-number":["16-CE91-0002"]}],"id":[{"id":"10.13039\/501100005304","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,1,14]]},"DOI":"10.1145\/3293880.3294096","type":"proceedings-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:56Z","timestamp":1546608836000},"page":"104-117","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines"],"prefix":"10.1145","author":[{"given":"Yannick","family":"Forster","sequence":"first","affiliation":[{"name":"Saarland University, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominique","family":"Larchey-Wendling","sequence":"additional","affiliation":[{"name":"University of Lorraine, France \/ CNRS, France \/ LORIA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,1,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.07.013"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Robert Berger. 1966. The undecidability of the domino problem. Number 66 in Memoirs of the American Mathematical Society. American Mathematical Soc.  Robert Berger. 1966. The undecidability of the domino problem. Number 66 in Memoirs of the American Mathematical Society. American Mathematical Soc.","DOI":"10.1090\/memo\/0066"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.06.019"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_13"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.02.004"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167088"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9361-9"},{"key":"e_1_3_2_1_9_1","volume-title":"Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. In ICALP 2017 (LIPIcs)","volume":"80","author":"Figueira Diego","year":"2017","unstructured":"Diego Figueira , Ranko Lazic , J\u00e9r\u00f4me Leroux , Filip Mazowiecki , and Gr\u00e9goire Sutre . 2017 . Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. In ICALP 2017 (LIPIcs) , Vol. 80 . Schloss Dagstuhl, 119:1\u201314. Diego Figueira, Ranko Lazic, J\u00e9r\u00f4me Leroux, Filip Mazowiecki, and Gr\u00e9goire Sutre. 2017. Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. In ICALP 2017 (LIPIcs), Vol. 80. Schloss Dagstuhl, 119:1\u201314."},{"key":"e_1_3_2_1_10_1","volume-title":"Verification of PCP-Related Computational Reductions in Coq. In International Conference on Interactive Theorem Proving. Springer, 253\u2013269","author":"Forster Yannick","year":"2018","unstructured":"Yannick Forster , Edith Heiter , and Gert Smolka . 2018 . Verification of PCP-Related Computational Reductions in Coq. In International Conference on Interactive Theorem Proving. Springer, 253\u2013269 . Yannick Forster, Edith Heiter, and Gert Smolka. 2018. Verification of PCP-Related Computational Reductions in Coq. In International Conference on Interactive Theorem Proving. Springer, 253\u2013269."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294091"},{"key":"e_1_3_2_1_12_1","volume-title":"Coq Workshop","author":"Forster Yannick","year":"2016","unstructured":"Yannick Forster and Fabian Kunze . 2016 . Verified Extraction from Coq to a Lambda-Calculus . In Coq Workshop 2016. Yannick Forster and Fabian Kunze. 2016. Verified Extraction from Coq to a Lambda-Calculus. In Coq Workshop 2016."},{"key":"e_1_3_2_1_13_1","volume-title":"Workshop on Syntax and Semantics of Low-level Languages","author":"Forster Yannick","year":"2018","unstructured":"Yannick Forster and Dominique Larchey-Wendling . 2018 . Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic . Workshop on Syntax and Semantics of Low-level Languages , Oxford (2018). Yannick Forster and Dominique Larchey-Wendling. 2018. Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic. Workshop on Syntax and Semantics of Low-level Languages, Oxford (2018)."},{"volume-title":"Interactive Theorem Proving - 8th International Conference","author":"Forster Yannick","key":"e_1_3_2_1_14_1","unstructured":"Yannick Forster and Gert Smolka . 2017. Weak call-by-value lambda calculus as a model of computation in Coq . In Interactive Theorem Proving - 8th International Conference , ITP. Springer , 189\u2013206. Yannick Forster and Gert Smolka. 2017. Weak call-by-value lambda calculus as a model of computation in Coq. In Interactive Theorem Proving - 8th International Conference, ITP. Springer, 189\u2013206."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/212876"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274135"},{"volume-title":"Computability and complexity: from a programming perspective","author":"Jones Neil D.","key":"e_1_3_2_1_18_1","unstructured":"Neil D. Jones . 1997. Computability and complexity: from a programming perspective . Vol. 21 . MIT press . Neil D. Jones. 1997. Computability and complexity: from a programming perspective. Vol. 21. MIT press."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90011-6"},{"key":"e_1_3_2_1_20_1","first-page":"123","article-title":"The direct simulation of Minsky machines in linear logic. See { 16 }","volume":"2","author":"Kanovich Max","year":"1995","unstructured":"Max Kanovich . 1995 . The direct simulation of Minsky machines in linear logic. See { 16 } , Chapter 2 , 123 \u2013 145 . Max Kanovich. 1995. The direct simulation of Minsky machines in linear logic. See { 16 }, Chapter 2, 123\u2013145.","journal-title":"Chapter"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863597.1863601"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"volume-title":"Interactive Theorem Proving - 8th International Conference","author":"Larchey-Wendling Dominique","key":"e_1_3_2_1_23_1","unstructured":"Dominique Larchey-Wendling . 2017. Typing Total Recursive Functions in Coq . In Interactive Theorem Proving - 8th International Conference , ITP. Springer , 371\u2013388. Dominique Larchey-Wendling. 2017. Typing Total Recursive Functions in Coq. In Interactive Theorem Proving - 8th International Conference, ITP. Springer, 371\u2013388."},{"key":"e_1_3_2_1_24_1","volume-title":"Proceedings. Springer, 422\u2013438","author":"Larchey-Wendling Dominique","year":"2018","unstructured":"Dominique Larchey-Wendling . 2018 . Constructive Decision via Redundancy-Free Proof-Search. In Automated Reasoning - 9th International Joint Conference, IJCAR , Proceedings. Springer, 422\u2013438 . Dominique Larchey-Wendling. 2018. Constructive Decision via Redundancy-Free Proof-Search. In Automated Reasoning - 9th International Joint Conference, IJCAR, Proceedings. Springer, 422\u2013438."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.18"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422085.2422091"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_28_1","first-page":"109","article-title":"Deciding provability of linear logic formulas. See { 16 }","volume":"2","author":"Lincoln Patrick","year":"1995","unstructured":"Patrick Lincoln . 1995 . Deciding provability of linear logic formulas. See { 16 } , Chapter 2 , 109 \u2013 122 . Patrick Lincoln. 1995. Deciding provability of linear logic formulas. See { 16 }, Chapter 2, 109\u2013122.","journal-title":"Chapter"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/FSCS.1990.89588"},{"key":"e_1_3_2_1_30_1","volume-title":"HOCore in Coq. In International Conference on Interactive Theorem Proving. Springer, 278\u2013293","author":"Maksimovi\u0107 Petar","year":"2015","unstructured":"Petar Maksimovi\u0107 and Alan Schmitt . 2015 . HOCore in Coq. In International Conference on Interactive Theorem Proving. Springer, 278\u2013293 . Petar Maksimovi\u0107 and Alan Schmitt. 2015. HOCore in Coq. In International Conference on Interactive Theorem Proving. Springer, 278\u2013293."},{"volume-title":"Computation: finite and infinite machines","author":"Minsky Marvin L.","key":"e_1_3_2_1_31_1","unstructured":"Marvin L. Minsky . 1967. Computation: finite and infinite machines . Prentice-Hall, Inc. Marvin L. Minsky. 1967. Computation: finite and infinite machines. Prentice-Hall, Inc."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/2033939.2033963"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-57669-4_11"},{"volume-title":"Theory of recursive functions and effective computability","author":"Rogers Hartley","key":"e_1_3_2_1_34_1","unstructured":"Hartley Rogers . 1967. Theory of recursive functions and effective computability . Vol. 5 . McGraw-Hill New York . Hartley Rogers. 1967. Theory of recursive functions and effective computability. Vol. 5. McGraw-Hill New York."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693163"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2893582.2893585"},{"key":"e_1_3_2_1_37_1","unstructured":"The Coq proof assistant. 2018. http:\/\/coq.inria.fr . (2018).  The Coq proof assistant. 2018. http:\/\/coq.inria.fr . (2018)."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_13"},{"volume-title":"A Proof of the S-m-n theorem in Coq. Technical report. The Computing Laboratory","author":"Zammit Vincent","key":"e_1_3_2_1_40_1","unstructured":"Vincent Zammit . 1997. A Proof of the S-m-n theorem in Coq. Technical report. The Computing Laboratory , The University of Kent , Canterbury, Kent, UK . http:\/\/kar.kent.ac.uk\/21524\/ Vincent Zammit. 1997. A Proof of the S-m-n theorem in Coq. Technical report. The Computing Laboratory, The University of Kent, Canterbury, Kent, UK. http:\/\/kar.kent.ac.uk\/21524\/"}],"event":{"name":"CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Cascais Portugal","acronym":"CPP '19"},"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.3294096","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293880.3294096","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:50Z","timestamp":1750207430000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294096"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,14]]},"references-count":39,"alternative-id":["10.1145\/3293880.3294096","10.1145\/3293880"],"URL":"https:\/\/doi.org\/10.1145\/3293880.3294096","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"}}]}}