{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:59Z","timestamp":1751660519075,"version":"3.41.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2018,7,30]],"date-time":"2018-07-30T00:00:00Z","timestamp":1532908800000},"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":[[2018,7,30]]},"abstract":"<jats:p>Dependent types are a powerful tool for maintaining program invariants. To take advantage of this aspect in real-world programming, efforts have been put into enriching dependently typed languages with missing constructs, most notably, effects. This paper presents a language that has two practically interesting ingredients: dependent inductive types, and the delimited control constructs shift and reset. When integrating delimited control into a dependently typed language, however, two challenges arise. First, the dynamic nature of control operators, which is the source of their expressiveness, can break fundamental language properties such as logical consistency and subject reduction. Second, CPS translations, which we often use to define the semantics of control operators, do not scale straightforwardly to dependently typed languages. We solve the former issue by restricting dependency of types, and the latter using answer-type polymorphism of pure terms. The main contribution of this paper is to give a sound type system of our language, as well as a type-preserving CPS translation. We also discuss various extensions, which would make our language more like a full-spectrum proof assistant but pose non-trivial issues.<\/jats:p>","DOI":"10.1145\/3236764","type":"journal-article","created":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T19:41:18Z","timestamp":1533066078000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Handling delimited continuations with dependent types"],"prefix":"10.1145","volume":"2","author":[{"given":"Youyou","family":"Cong","sequence":"first","affiliation":[{"name":"Ochanomizu University, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kenichi","family":"Asai","sequence":"additional","affiliation":[{"name":"Ochanomizu University, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,7,30]]},"reference":[{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158095"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034830"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/647849.737066"},{"key":"e_1_2_2_5_1","volume-title":"The Third International Workshop on Coq for Programming Languages (CoqPL).","author":"Anand Abhishek","year":"2017","unstructured":"Abhishek Anand , A Appel , Greg Morrisett , Zoe Paraskevopoulou , Randy Pollack , Olivier Savary B\u00e9langer , Matthieu Sozeau , and Matthew Weaver . 2017 . CertiCoq: A verified compiler for Coq . In The Third International Workshop on Coq for Programming Languages (CoqPL). Abhishek Anand, A Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary B\u00e9langer, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. In The Third International Workshop on Coq for Programming Languages (CoqPL)."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9006-0"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1784774.1784797"},{"key":"e_1_2_2_8_1","volume-title":"ACM SIGPLAN Continuation Workshop","author":"Asai Kenichi","year":"2011","unstructured":"Kenichi Asai and Oleg Kiselyov . 2011 . Introduction to programming with shift and reset . In ACM SIGPLAN Continuation Workshop 2011. Kenichi Asai and Oleg Kiselyov. 2011. Introduction to programming with shift and reset. In ACM SIGPLAN Continuation Workshop 2011."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3162069"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010000206149"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/503032.503043"},{"key":"e_1_2_2_12_1","volume-title":"JFLA - Journ\u00e9es Francophones des langages applicatifs -","author":"Boutillier Pierre","year":"2012","unstructured":"Pierre Boutillier . 2012. A relaxation of Coq\u2019s guard condition . In JFLA - Journ\u00e9es Francophones des langages applicatifs - 2012 . Carnac , France , 1 \u2013 14. https:\/\/hal.archives- ouvertes.fr\/hal- 00651780 Pierre Boutillier. 2012. A relaxation of Coq\u2019s guard condition. In JFLA - Journ\u00e9es Francophones des langages applicatifs - 2012. Carnac, France, 1 \u2013 14. https:\/\/hal.archives- ouvertes.fr\/hal- 00651780"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158110"},{"key":"e_1_2_2_14_1","volume-title":"Handling Delimited Continuations with Dependent Types (Technical Appendix). (June","author":"Cong Youyou","year":"2018","unstructured":"Youyou Cong and Kenichi Asai . 2018. Handling Delimited Continuations with Dependent Types (Technical Appendix). (June 2018 ). https:\/\/github.com\/YouyouCong\/icfp18\/ Youyou Cong and Kenichi Asai. 2018. Handling Delimited Continuations with Dependent Types (Technical Appendix). (June 2018). https:\/\/github.com\/YouyouCong\/icfp18\/"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/646125.758641"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/357766.351262"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237784"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Olivier Danvy and Andrzej Filinski. 1992. Representing control: a study of the CPS transformation.  Olivier Danvy and Andrzej Filinski. 1992. Representing control: a study of the CPS transformation.","DOI":"10.1017\/S0960129500001535"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178047"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291178"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110257"},{"volume-title":"Selected Papers from the International Workshop on Types for Proofs and Programs (TYPES \u201994)","author":"Gim\u00e9nez Eduardo","key":"e_1_2_2_26_1","unstructured":"Eduardo Gim\u00e9nez . 1995. Codifying Guarded Definitions with Recursive Schemes . In Selected Papers from the International Workshop on Types for Proofs and Programs (TYPES \u201994) . Springer-Verlag , London, UK , 39\u201359. http:\/\/dl.acm.org\/citation. cfm?id=646535.695850 Eduardo Gim\u00e9nez. 1995. Codifying Guarded Definitions with Recursive Schemes. In Selected Papers from the International Workshop on Types for Proofs and Programs (TYPES \u201994). Springer-Verlag, London, UK, 39\u201359. http:\/\/dl.acm.org\/citation. cfm?id=646535.695850"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_16"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.47"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328484"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.12.008"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706333"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480945.1480962"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159808"},{"key":"e_1_2_2_37_1","volume-title":"ML Workshop.","author":"Kiselyov Oleg","year":"2016","unstructured":"Oleg Kiselyov and KC Sivaramakrishnan . 2016 . Eff directly in OCaml . In ML Workshop. Oleg Kiselyov and KC Sivaramakrishnan. 2016. Eff directly in OCaml. In ML Workshop."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9008-y"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_19"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_2_41_1","volume-title":"Call-by-push-value: A Functional\/imperative Synthesis.","author":"Levy Paul Blain","year":"2012","unstructured":"Paul Blain Levy . 2012 . Call-by-push-value: A Functional\/imperative Synthesis. Vol. 2 . Springer Science & amp; Business Media. Paul Blain Levy. 2012. Call-by-push-value: A Functional\/imperative Synthesis. Vol. 2. Springer Science &amp; Business Media."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034786"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/645706.663989"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/645736.666272"},{"key":"e_1_2_2_46_1","unstructured":"Chung-Chieh Shan. 2003. From shift and reset to polarized linear logic. (2003). Unpublished.  Chung-Chieh Shan. 2003. From shift and reset to polarized linear logic. (2003). Unpublished."},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9010-4"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29822-6_21"},{"key":"e_1_2_2_52_1","unstructured":"The Coq Development Team. 2018. The Coq Proof Assistant Reference Manual. https:\/\/coq.inria.fr\/refman\/  The Coq Development Team. 2018. The Coq Proof Assistant Reference Manual. https:\/\/coq.inria.fr\/refman\/"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604144"},{"key":"e_1_2_2_54_1","unstructured":"Matthijs V\u00e1k\u00e1r. 2017. In Search of Effectful Dependent Types. Ph.D. Dissertation. Oxford University.  Matthijs V\u00e1k\u00e1r. 2017. In Search of Effectful Dependent Types. Ph.D. Dissertation. Oxford University."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.23"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236764","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236764","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:41:28Z","timestamp":1750282888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236764"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,30]]},"references-count":51,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2018,7,30]]}},"alternative-id":["10.1145\/3236764"],"URL":"https:\/\/doi.org\/10.1145\/3236764","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2018,7,30]]},"assertion":[{"value":"2018-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}