{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:24Z","timestamp":1772163984029,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T00:00:00Z","timestamp":1380067200000},"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":[],"published-print":{"date-parts":[[2013,9,25]]},"DOI":"10.1145\/2500365.2500593","type":"proceedings-article","created":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T09:13:17Z","timestamp":1380100397000},"page":"363-376","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Hoare-style reasoning with (algebraic) continuations"],"prefix":"10.1145","author":[{"given":"Germ\u00e1n Andr\u00e9s","family":"Delbianco","sequence":"first","affiliation":[{"name":"IMDEA Software Institute, Pozuelo de Alarc\u00f3n, Spain"}]},{"given":"Aleksandar","family":"Nanevski","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Pozuelo de Alarc\u00f3n, Spain"}]}],"member":"320","published-online":{"date-parts":[[2013,9,25]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"91","author":"ACETO L.","year":"2007","unstructured":"ACETO , L. , AND INGOLFSDOTTIR , A. Characteristic formulae: From automata to logic. Bulletin of the EATCS 91 ( 2007 ). ACETO, L., AND INGOLFSDOTTIR, A. Characteristic formulae: From automata to logic. Bulletin of the EATCS 91 (2007).","journal-title":"Bulletin of the EATCS"},{"key":"e_1_3_2_1_2_1","first-page":"11","author":"ARBIB M. A.","year":"1979","unstructured":"ARBIB , M. A. , AND ALAGIC , S. Proof rules for gotos. Acta Inf. 11 ( 1979 ). ARBIB, M. A., AND ALAGIC, S. Proof rules for gotos. Acta Inf. 11 (1979).","journal-title":"Acta Inf."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792803.1792829"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/503032.503043"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11623-0_11"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/647529"},{"key":"e_1_3_2_1_9_1","first-page":"1","author":"CLINT M.","year":"1972","unstructured":"CLINT , M. , AND HOARE , C. A. R. Program proving: Jumps and functions. Acta Inf. 1 ( 1972 ). CLINT, M., AND HOARE, C. A. R. Program proving: Jumps and functions. Acta Inf. 1 (1972).","journal-title":"Acta Inf."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.004"},{"key":"e_1_3_2_1_11_1","first-page":"4","volume":"2","author":"DANVY O.","year":"1992","unstructured":"DANVY , O. , AND FILINSKI , A. Representing control: A study of the CPS transformation. MSCS 2 , 4 ( 1992 ). DANVY, O., AND FILINSKI, A. Representing control: A study of the CPS transformation. MSCS 2, 4 (1992).","journal-title":"MSCS"},{"key":"e_1_3_2_1_12_1","unstructured":"DELBIANCO G. A. AND NANEVSKI A. Supporting material. http:\/\/software.imdea.org\/~germand\/HTTcc March 2013.  DELBIANCO G. A. AND NANEVSKI A. Supporting material. http:\/\/software.imdea.org\/~germand\/HTTcc March 2013."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863566"},{"key":"e_1_3_2_1_14_1","volume-title":"Indiana University","author":"FELLEISEN M.","year":"1987","unstructured":"FELLEISEN , M. , FRIEDMAN , D. P. , DUBA , B. , AND MERRILL , J. Beyond Continuations. Tech. Rep. 216 , Indiana University , 1987 . FELLEISEN, M., FRIEDMAN, D. P., DUBA, B., AND MERRILL, J. Beyond Continuations. Tech. Rep. 216, Indiana University, 1987."},{"key":"e_1_3_2_1_15_1","volume-title":"LICS","author":"FELLEISEN M.","year":"1986","unstructured":"FELLEISEN , M. , FRIEDMAN , D. P. , KOHLBECKER , E. E. , AND DUBA , B. F. Reasoning with continuations . In LICS ( 1986 ). FELLEISEN, M., FRIEDMAN, D. P., KOHLBECKER, E. E., AND DUBA, B. F. Reasoning with continuations. In LICS (1986)."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/62678.62684"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178047"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/230222"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.026"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_6"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429105"},{"key":"e_1_3_2_1_24_1","first-page":"11","author":"KLEYMANN T.","year":"1999","unstructured":"KLEYMANN , T. Hoare logic and auxiliary variables. Formal Aspects of Computing 11 ( 1999 ). KLEYMANN, T. Hoare logic and auxiliary variables. Formal Aspects of Computing 11 (1999).","journal-title":"Formal Aspects of Computing"},{"key":"e_1_3_2_1_25_1","first-page":"7","author":"KOWALTOWSKI T.","year":"1977","unstructured":"KOWALTOWSKI , T. Axiomatic approach to side effects and general jumps. Acta Inf. 7 ( 1977 ). KOWALTOWSKI, T. Axiomatic approach to side effects and general jumps. Acta Inf. 7 (1977).","journal-title":"Acta Inf."},{"key":"e_1_3_2_1_27_1","volume-title":"TypiCal Project","author":"THE COQ DEVELOPMENT TEAM","year":"2012","unstructured":"THE COQ DEVELOPMENT TEAM . The Coq proof assistant reference manual . TypiCal Project , 2012 . Version 8.4. THE COQ DEVELOPMENT TEAM. The Coq proof assistant reference manual. TypiCal Project, 2012. Version 8.4."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77353"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706331"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/647210.720030"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.08.008"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/317040"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019459"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.020"},{"key":"e_1_3_2_1_39_1","first-page":"3","volume":"7","author":"SCHWINGHAMMER J.","year":"2011","unstructured":"SCHWINGHAMMER , J. , BIRKEDAL , L. , REUS , B. , AND YANG , H. Nested Hoare triples and frame rules for higher-order store. LMCS 7 , 3 ( 2011 ). SCHWINGHAMMER, J., BIRKEDAL, L., REUS, B., AND YANG, H. Nested Hoare triples and frame rules for higher-order store. LMCS 7, 3 (2011).","journal-title":"LMCS"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/75029"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190244"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010026413531"},{"key":"e_1_3_2_1_43_1","volume-title":"TLCA","author":"SVENDSEN K.","year":"2011","unstructured":"SVENDSEN , K. , BIRKEDAL , L. , AND NANEVSKI , A. Partiality , state and dependent types . In TLCA ( 2011 ). SVENDSEN, K., BIRKEDAL, L., AND NANEVSKI, A. Partiality, state and dependent types. In TLCA (2011)."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_30"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_6"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006734"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019944"},{"key":"e_1_3_2_1_50_1","first-page":"4","volume":"4","author":"YOSHIDA N.","year":"2008","unstructured":"YOSHIDA , N. , HONDA , K. , AND BERGER , M. Logical reasoning for higher-order functions with local state. LMCS 4 , 4 ( 2008 ). YOSHIDA, N., HONDA, K., AND BERGER, M. Logical reasoning for higher-order functions with local state. LMCS 4, 4 (2008).","journal-title":"LMCS"}],"event":{"name":"ICFP'13: ACM SIGPLAN International Conference on Functional Programming","location":"Boston Massachusetts USA","acronym":"ICFP'13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","Northeastern University"]},"container-title":["Proceedings of the 18th ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2500365.2500593","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2500365.2500593","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:34:32Z","timestamp":1750217672000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2500365.2500593"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,25]]},"references-count":46,"alternative-id":["10.1145\/2500365.2500593","10.1145\/2500365"],"URL":"https:\/\/doi.org\/10.1145\/2500365.2500593","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2544174.2500593","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,9,25]]},"assertion":[{"value":"2013-09-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}