{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,12]],"date-time":"2024-08-12T18:38:06Z","timestamp":1723487886075},"reference-count":24,"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":"http:\/\/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":"We present a logical relations model of a higher-order functional programming language with impredicative polymorphism, recursive types, and a Haskell-style ST monad type with runST. We use our logical relations model to show that runST provides proper encapsulation of state, by showing that effectful computations encapsulated by runST are heap independent. Furthermore, we show that contextual refinements and equivalences that are expected to hold for pure computations do indeed hold in the presence of runST. This is the first time such relational results have been proven for a language with monadic encapsulation of state. We have formalized all the technical development and results in Coq.<\/jats:p>","DOI":"10.1145\/3158152","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-28","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST"],"prefix":"10.1145","volume":"2","author":[{"given":"Amin","family":"Timany","sequence":"first","affiliation":[{"name":"KU Leuven, Belgium"}]},{"given":"L\u00e9o","family":"Stefanesco","sequence":"additional","affiliation":[{"name":"IRIF, France \/ CNRS, France \/ University of Paris Diderot, France"}]},{"given":"Morten","family":"Krogh-Jespersen","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029818"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_5_1","doi-asserted-by":"crossref","unstructured":"Andrew Appel Paul-Andr\u00e9 Melli\u00e8s Christopher Richards and J\u00e9r\u00f4me Vouillon. 2007. A Very Modal Model of a Modern Major General Type System. In POPL. Andrew Appel Paul-Andr\u00e9 Melli\u00e8s Christopher Richards and J\u00e9r\u00f4me Vouillon. 2007. A Very Modal Model of a Modern Major General Type System. In POPL.","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190320"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273920.1273932"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599447"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11924661_7"},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Lars Birkedal Bernhard Reus Jan Schwinghammer Kristian St\u00f8vring Jacob Thamsborg and Hongseok Yang. 2011. StepIndexed Kripke Models over Recursive Worlds. In POPL. Lars Birkedal Bernhard Reus Jan Schwinghammer Kristian St\u00f8vring Jacob Thamsborg and Hongseok Yang. 2011. StepIndexed Kripke Models over Recursive Worlds. In POPL.","DOI":"10.1145\/1926385.1926401"},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"D. Dreyer A. Ahmed and L. Birkedal. 2011. Logical Step-Indexed Logical Relations. LMCS 7 2:16 (2011). D. Dreyer A. Ahmed and L. Birkedal. 2011. Logical Step-Indexed Logical Relations. LMCS 7 2:16 (2011).","DOI":"10.2168\/LMCS-7(2:16)2011"},{"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\/319838.319848"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_15_1","volume-title":"Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. 637\u2013650.","author":"Jung Ralf","year":"2015"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009877"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178246"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018827"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004154"},{"key":"e_1_2_2_22_1","volume-title":"Information Processing","author":"Reynolds John C.","year":"1983"},{"key":"e_1_2_2_23_1","first-page":"359","article-title":"Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions","volume":"9236","author":"Sch\u00e4fer Steven","year":"2015","journal-title":"ITP (LNCS)"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317777"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034831"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158152","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T19:36:19Z","timestamp":1672515379000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158152"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":24,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158152"],"URL":"https:\/\/doi.org\/10.1145\/3158152","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"}}]}}