{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:48Z","timestamp":1775790768093,"version":"3.50.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>\n            This paper considers verification of\n            <jats:italic>non-deterministic<\/jats:italic>\n            higher-order functional programs. Our contribution is a novel type system in which the types are used to express and verify (conditional) safety, termination, non-safety, and non-termination properties in the presence of \u2200-\u2203 branching behavior due to non-determinism. For instance, the judgement \u22a2\n            <jats:italic>e<\/jats:italic>\n            :{\n            <jats:italic>u<\/jats:italic>\n            :\n            <jats:italic>int<\/jats:italic>\n            | \u03c6(\n            <jats:italic>u<\/jats:italic>\n            ) }\n            <jats:sup>\u2200\u2200<\/jats:sup>\n            says that every evaluation of\n            <jats:italic>e<\/jats:italic>\n            either diverges or reduces to some integer\n            <jats:italic>u<\/jats:italic>\n            satisfying \u03c6(\n            <jats:italic>u<\/jats:italic>\n            ), whereas \u22a2\n            <jats:italic>e<\/jats:italic>\n            :{\n            <jats:italic>u<\/jats:italic>\n            :\n            <jats:italic>int<\/jats:italic>\n            | \u03c8(\n            <jats:italic>u<\/jats:italic>\n            ) }\n            <jats:sup>\u2203\u2200<\/jats:sup>\n            says that there exists an evaluation of\n            <jats:italic>e<\/jats:italic>\n            that either diverges or reduces to some integer\n            <jats:italic>u<\/jats:italic>\n            satisfying \u03c8(\n            <jats:italic>u<\/jats:italic>\n            ). Note that the former is a safety property whereas the latter is a counterexample to a (conditional) termination property. Following the recent work on type-based verification methods for deterministic higher-order functional programs, we formalize the idea on the foundation of\n            <jats:italic>dependent refinement types<\/jats:italic>\n            , thereby allowing the type system to express and verify rich properties involving program values, branching behaviors, and the combination thereof.\n          <\/jats:p>\n          <jats:p>Our type system is able to seamlessly combine deductions of both universal and existential facts within a unified framework, paving the way for an exciting opportunity for new type-based verification methods that combine both universal and existential reasoning. For example, our system can prove the existence of a path violating some safety property from a proof of termination that uses a well-foundedness termination argument. We prove that our type system is sound and relatively complete, and further, thanks to having both modes of non-determinism, we show that our types are closed under complement.<\/jats:p>","DOI":"10.1145\/3158100","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Relatively complete refinement type system for verification of higher-order non-deterministic programs"],"prefix":"10.1145","volume":"2","author":[{"given":"Hiroshi","family":"Unno","sequence":"first","affiliation":[{"name":"University of Tsukuba, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuki","family":"Satake","sequence":"additional","affiliation":[{"name":"University of Tsukuba, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tachio","family":"Terauchi","sequence":"additional","affiliation":[{"name":"Waseda University, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_8"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958062"},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St","author":"Bod\u00edk Rastislav","year":"2016","unstructured":"Rastislav Bod\u00edk and Rupak Majumdar ( Eds .). 2016 . Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St . Petersburg, FL, USA, January 20 - 22 , 2016. ACM. http:\/\/dl.acm.org\/ citation.cfm?id=2837614 Rastislav Bod\u00edk and Rupak Majumdar (Eds.). 2016. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. ACM. http:\/\/dl.acm.org\/ citation.cfm?id=2837614"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_11"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_2"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491969"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264295"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzn018"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12896-4_365"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90040-0"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.28"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44685-0_29"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706307"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15648-8_9"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_14"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_18"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88387-6_9"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_12"},{"key":"e_1_2_2_22_1","volume-title":"Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010","author":"Manuel","year":"2010","unstructured":"Manuel V. Hermenegildo and Jens Palsberg (Eds.). 2010 . Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010 , Madrid, Spain , January 17-23, 2010 . ACM. http:\/\/dl.acm.org\/citation. cfm?id=1706299 Manuel V. Hermenegildo and Jens Palsberg (Eds.). 2010. Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. ACM. http:\/\/dl.acm.org\/citation. cfm?id=1706299"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_31"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_38"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"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\/1993498.1993525"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603138"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_17"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_21"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837667"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90066-5"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926453"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_17"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2011.470"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_40"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297658.1297659"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706315"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599445"},{"key":"e_1_2_2_44_1","doi-asserted-by":"crossref","unstructured":"Hiroshi Unno Yuki Satake and Tachio Terauchi. 2017. Relatively Complete Refinement Type System for Verification of Higher-Order Non-Deterministic Programs. Extended version available from http:\/\/www.cs.tsukuba.ac.jp\/~uhiro\/ .  Hiroshi Unno Yuki Satake and Tachio Terauchi. 2017. Relatively Complete Refinement Type System for Verification of Higher-Order Non-Deterministic Programs. Extended version available from http:\/\/www.cs.tsukuba.ac.jp\/~uhiro\/ .","DOI":"10.1145\/3158100"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429081"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932500"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_19"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784766"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158100","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158100","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158100"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":49,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158100"],"URL":"https:\/\/doi.org\/10.1145\/3158100","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}