{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:44Z","timestamp":1780994684769,"version":"3.54.1"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>Type-and-effect systems are a widely used approach to program verification, verifying the result of a computation using types, and its behavior using effects. This paper extends an effect system for verifying temporal, value-dependent properties on event sequences yielded by programs, to the delimited control operators shift0\/reset0. While these delimited control operators enable useful and powerful programming techniques, they hinder reasoning about the behavior of programs because of their ability to suspend, resume, discard, and duplicate delimited continuations. This problem is more serious in effect systems for temporal properties because these systems must be capable of identifying what event sequences are yielded by captured continuations. Our key observation for achieving effective reasoning in the presence of the delimited control operators is that their use modifies answer effects, which are temporal effects of the continuations. Based on this observation, we extend an effect system for temporal verification to accommodate answer-effect modification. Allowing answer-effect modification enables easily reasoning about traces that captured continuations yield. Another novel feature of our effect system is the support for dependently typed continuations, which allows us to reason about programs more precisely. We prove soundness of the effect system for finite event sequences via type safety and that for infinite event sequences using a logical relation.<\/jats:p>","DOI":"10.1145\/3571264","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"2079-2110","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-230X","authenticated-orcid":false,"given":"Taro","family":"Sekiyama","sequence":"first","affiliation":[{"name":"National Institute of Informatics, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8195","authenticated-orcid":false,"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[{"name":"University of Tsukuba, Japan \/ RIKEN AIP, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158095"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1639950.1640073"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.06.007"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567080"},{"key":"e_1_2_2_6_1","volume-title":"A Scheme for a Higher-Level Semantic Algebra","author":"Clinger William D.","unstructured":"William D. Clinger , Daniel P. Friedman , and Mitchell Wand . 1985. A Scheme for a Higher-Level Semantic Algebra . Cambridge University Press , 237\u2013250. William D. Clinger, Daniel P. Friedman, and Mitchell Wand. 1985. A Scheme for a Higher-Level Semantic Algebra. Cambridge University Press, 237\u2013250."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236764"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3060257"},{"key":"e_1_2_2_9_1","unstructured":"Olivier Danvy and Andrzej Filinski. 1989. A functional abstraction of typed contexts. \t\t\t\t  Olivier Danvy and Andrzej Filinski. 1989. A functional abstraction of typed contexts."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178047"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110257"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.13"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.23"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450272"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224173"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_16"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.47"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603127"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503303"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111542.1111550"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78969-7_18"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_20"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603138"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_19"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481868"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0061"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034786"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_29"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837667"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_2_2_38_1","doi-asserted-by":"crossref","unstructured":"Yoji Nanjo Hiroshi Unno Eric Koskinen and Tachio Terauchi. 2018. A Fixpoint Logic and Dependent Effects for Temporal Property Verification. https:\/\/www.cs.tsukuba.ac.jp\/~uhiro\/papers\/lics2018full.pdf Technical report extending t Nanjo\/Unno\/Koskinen\/Terauchi_2018_LICS with proofs \t\t\t\t  Yoji Nanjo Hiroshi Unno Eric Koskinen and Tachio Terauchi. 2018. A Fixpoint Logic and Dependent Effects for Temporal Property Verification. https:\/\/www.cs.tsukuba.ac.jp\/~uhiro\/papers\/lics2018full.pdf Technical report extending t Nanjo\/Unno\/Koskinen\/Terauchi_2018_LICS with proofs","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19195-9_1"},{"key":"e_1_2_2_40_1","volume-title":"Higher Order Operational Techniques in Semantics","author":"Pitts Andrew","unstructured":"Andrew Pitts and Ian Stark . 1998. Operational Reasoning for Functions with Local State . In Higher Order Operational Techniques in Semantics , Andrew Gordon and Andrew Pitts (Eds.). Publications of the Newton Institute, Cambridge University Press , 227\u2013273. http:\/\/www.inf.ed.ac.uk\/~stark\/operfl.html Andrew Pitts and Ian Stark. 1998. Operational Reasoning for Functions with Local State. In Higher Order Operational Techniques in Semantics, Andrew Gordon and Andrew Pitts (Eds.). Publications of the Newton Institute, Cambridge University Press, 227\u2013273. http:\/\/www.inf.ed.ac.uk\/~stark\/operfl.html"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80685-1"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_45_1","volume-title":"Proceedings of the 5th workshop on Scheme and Functional Programming, Olin Shivers and Oscar Waddell (Eds.). 99\u2013107","year":"2004","unstructured":"Chung-chieh Shan. 2004 . Shift to Control . In Proceedings of the 5th workshop on Scheme and Functional Programming, Olin Shivers and Oscar Waddell (Eds.). 99\u2013107 . Chung-chieh Shan. 2004. Shift to Control. In Proceedings of the 5th workshop on Scheme and Functional Programming, Olin Shivers and Oscar Waddell (Eds.). 99\u2013107."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_8"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599445"},{"key":"e_1_2_2_50_1","volume-title":"Program Verification via Predicate Constraint Satisfiability Modulo Theories. CoRR, abs\/2007.03656","author":"Unno Hiroshi","year":"2020","unstructured":"Hiroshi Unno , Yuki Satake , Tachio Terauchi , and Eric Koskinen . 2020. Program Verification via Predicate Constraint Satisfiability Modulo Theories. CoRR, abs\/2007.03656 ( 2020 ), arXiv:2007.03656. arxiv:2007.03656 Hiroshi Unno, Yuki Satake, Tachio Terauchi, and Eric Koskinen. 2020. Program Verification via Predicate Constraint Satisfiability Modulo Theories. CoRR, abs\/2007.03656 (2020), arXiv:2007.03656. arxiv:2007.03656"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_24"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571264","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571264","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:22Z","timestamp":1750183702000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571264"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":51,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571264"],"URL":"https:\/\/doi.org\/10.1145\/3571264","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}