{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:15:48Z","timestamp":1787062548906,"version":"build-2736575974"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP20H05703"],"award-info":[{"award-number":["JP20H05703"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>The decidability of the reachability problem for finitary PCF has been used as a theoretical basis for fully automated verification tools for functional programs. The reachability problem, however, often becomes undecidable for a slight extension of finitary PCF with side effects, such as exceptions, algebraic effects, and references, which hindered the extension of the above verification tools for supporting functional programs with side effects. In this paper, we first give simple proofs of the undecidability of four extensions of finitary PCF, which would help us understand and analyze the source of undecidability. We then focus on an extension with references, and give a decidable fragment using a type system. To our knowledge, this is the first non-trivial decidable fragment that features higher-order recursive functions containing reference cells.<\/jats:p>","DOI":"10.1145\/3704875","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1136-1166","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0537-0604","authenticated-orcid":false,"given":"Naoki","family":"Kobayashi","sequence":"first","affiliation":[{"name":"The University of Tokyo, Tokyo, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-007-0044-Z"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_18"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2013.129"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_22"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371127"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/322063.322074"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3418295"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599415"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_18"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487246"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Naoki Kobayashi . 2024. On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus. https:\/\/doi.org\/10.48550\/arXiv.2411.06086 10.48550\/arXiv.2411.06086 arXiv:2411.06086 [cs.PL] A longer version.","DOI":"10.48550\/arXiv.2411.06086"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706355"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632929"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010020917337"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094626"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2004.12.036"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.24"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_74"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_13"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-50521-8_11"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.APAL.2003.12.006"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926453"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.48"},{"key":"e_1_3_2_37_2","first-page":"227","volume-title":"Operational reasoning for functions with local state","author":"Pitts A. M.","year":"1999","unstructured":"A. M. Pitts and I. D. B. Stark. 1999. Operational reasoning for functions with local state. Cambridge University Press, USA, 227\u2013274."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535873"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/2426890.2426900"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_25"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54830-7_12"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704875","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704875","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:18:11Z","timestamp":1770200291000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704875"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":41,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704875"],"URL":"https:\/\/doi.org\/10.1145\/3704875","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}