{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:19Z","timestamp":1750220659533,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Paris Ile-de-France Region"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,7,8]]},"DOI":"10.1145\/3373718.3394792","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:23:18Z","timestamp":1590452598000},"page":"564-577","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A calculus of expandable stores"],"prefix":"10.1145","author":[{"given":"Hugo","family":"Herbelin","sequence":"first","affiliation":[{"name":"INRIA, IRIF (CNRS), Universit\u00e9 Paris-Diderot, France"}]},{"given":"\u00c9tienne","family":"Miquey","sequence":"additional","affiliation":[{"name":"CNRS, LSV, INRIA, \u00c9NS Paris-Saclay, France"}]}],"member":"320","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96712"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628154"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3131851.3131855"},{"volume-title":"Compiling with Continuations","author":"Appel Andrew W.","key":"e_1_3_2_1_4_1","unstructured":"Andrew W. Appel . 1992. Compiling with Continuations . Cambridge University Press , New York, NY, USA . Andrew W. Appel. 1992. Compiling with Continuations. Cambridge University Press, New York, NY, USA."},{"key":"e_1_3_2_1_5_1","volume-title":"FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings (Lecture Notes in Computer Science), Tom Schrijvers and Peter Thiemann (Eds.)","author":"Ariola Zena M.","year":"2012","unstructured":"Zena M. Ariola , Paul Downen , Hugo Herbelin , Keiko Nakata , and Alexis Saurin . 2012 . Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts. In Functional and Logic Programming - 11th International Symposium , FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings (Lecture Notes in Computer Science), Tom Schrijvers and Peter Thiemann (Eds.) . Springer, New York, NY, USA, 32--46. https: \/\/doi.org\/10.1007\/978-3-642-29822-6 10.1007\/978-3-642-29822-6 Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, and Alexis Saurin. 2012. Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts. In Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings (Lecture Notes in Computer Science), Tom Schrijvers and Peter Thiemann (Eds.). Springer, New York, NY, USA, 32--46. https: \/\/doi.org\/10.1007\/978-3-642-29822-6"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"volume-title":"An extension of system F with subtyping","author":"Cardelli Luca","key":"e_1_3_2_1_7_1","unstructured":"Luca Cardelli , Simone Martini , John C. Mitchell , and Andre Scedrov . 1991. An extension of system F with subtyping . Springer Berlin Heidelberg , Berlin, Heidelberg , 750--770. http:\/\/dx.doi.org\/10.1007\/3-540-54415-1_73 10.1007\/3-540-54415-1_73 Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. 1991. An extension of system F with subtyping. Springer Berlin Heidelberg, Berlin, Heidelberg, 750--770. http:\/\/dx.doi.org\/10.1007\/3-540-54415-1_73"},{"key":"e_1_3_2_1_8_1","volume-title":"Strongly reducing variants of the Krivine abstract machine. Higher-Order and Symbolic Computation 20, 3 (01","author":"Cr\u00e9gut Pierre","year":"2007","unstructured":"Pierre Cr\u00e9gut . 2007. Strongly reducing variants of the Krivine abstract machine. Higher-Order and Symbolic Computation 20, 3 (01 Sep 2007 ), 209--230. https:\/\/doi.org\/10.1007\/s10990-007-9015-z 10.1007\/s10990-007-9015-z Pierre Cr\u00e9gut. 2007. Strongly reducing variants of the Krivine abstract machine. Higher-Order and Symbolic Computation 20, 3 (01 Sep 2007), 209--230. https:\/\/doi.org\/10.1007\/s10990-007-9015-z"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"volume-title":"3rd Working Conference on the Formal Description of Programming Concepts. North-Holland","author":"Felleisen Matthias","key":"e_1_3_2_1_11_1","unstructured":"Matthias Felleisen and Daniel P. Friedman . 1986. Control operators, the SECD-machine, and the lambda-calculus . In 3rd Working Conference on the Formal Description of Programming Concepts. North-Holland , New York, NY, USA, 193--217. Matthias Felleisen and Daniel P. Friedman. 1986. Control operators, the SECD-machine, and the lambda-calculus. In 3rd Working Conference on the Formal Description of Programming Concepts. North-Holland, New York, NY, USA, 193--217."},{"key":"e_1_3_2_1_12_1","unstructured":"Matthias Felleisen and Amir Sabry. 1999. Continuations in programming practice: Introduction and survey. (1999). https:\/\/www.cs.indiana. edu\/~sabry\/papers\/continuations.ps Manuscript.  Matthias Felleisen and Amir Sabry. 1999. Continuations in programming practice: Introduction and survey. (1999). https:\/\/www.cs.indiana. edu\/~sabry\/papers\/continuations.ps Manuscript."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935320"},{"key":"e_1_3_2_1_15_1","article-title":"Semantical Considerations on Modal Logic","volume":"16","author":"Kripke Saul A.","year":"1963","unstructured":"Saul A. Kripke . 1963 . Semantical Considerations on Modal Logic . Acta Philosophica Fennica 16 , 1963 (1963), 83--94. Saul A. Kripke. 1963. Semantical Considerations on Modal Logic. Acta Philosophica Fennica 16, 1963 (1963), 83--94.","journal-title":"Acta Philosophica Fennica"},{"volume-title":"Higher Order and Symbolic Computation","author":"Krivine Jean-Louis","key":"e_1_3_2_1_16_1","unstructured":"Jean-Louis Krivine . 2007. A call-by-name lambda-calculus machine . In Higher Order and Symbolic Computation , Vol. 20 . Springer , New York, NY, USA , 199--207. https:\/\/doi.org\/10.1007\/s10990-007-9018-9 10.1007\/s10990-007-9018-9 Jean-Louis Krivine. 2007. A call-by-name lambda-calculus machine. In Higher Order and Symbolic Computation, Vol. 20. Springer, New York, NY, USA, 199--207. https:\/\/doi.org\/10.1007\/s10990-007-9018-9"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(3:2)2011"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_3_2_1_19_1","volume-title":"Explaining the lazy Krivine machine using explicit substitution and addresses. Higher-Order and Symbolic Computation 20, 3 (01","author":"Lang Fr\u00e9d\u00e9ric","year":"2007","unstructured":"Fr\u00e9d\u00e9ric Lang . 2007. Explaining the lazy Krivine machine using explicit substitution and addresses. Higher-Order and Symbolic Computation 20, 3 (01 Sep 2007 ), 257--270. https:\/\/doi.org\/10.1007\/s10990-007-9013-1 10.1007\/s10990-007-9013-1 Fr\u00e9d\u00e9ric Lang. 2007. Explaining the lazy Krivine machine using explicit substitution and addresses. Higher-Order and Symbolic Computation 20, 3 (01 Sep 2007), 257--270. https:\/\/doi.org\/10.1007\/s10990-007-9013-1"},{"key":"e_1_3_2_1_20_1","unstructured":"Xavier Leroy. 1990. The ZINC experiment: an economical implementation of the ML language. Technical report 117. INRIA.  Xavier Leroy. 1990. The ZINC experiment: an economical implementation of the ML language. Technical report 117. INRIA."},{"volume-title":"Sheaves in Geometry and Logic","author":"MacLane Saunders","key":"e_1_3_2_1_21_1","unstructured":"Saunders MacLane and Ieke Moerdijk . 1992. Sheaves in Geometry and Logic . Springer , New York, NY, USA . https:\/\/doi.org\/10.1007\/978-1-4612-0927-0 10.1007\/978-1-4612-0927-0 Saunders MacLane and Ieke Moerdijk. 1992. Sheaves in Geometry and Logic. Springer, New York, NY, USA. https:\/\/doi.org\/10.1007\/978-1-4612-0927-0"},{"volume-title":"Local States in String Diagrams","author":"Melli\u00e8s Paul-Andr\u00e9","key":"e_1_3_2_1_22_1","unstructured":"Paul-Andr\u00e9 Melli\u00e8s . 2014. Local States in String Diagrams . Springer International Publishing , Cham , 334--348. Paul-Andr\u00e9 Melli\u00e8s. 2014. Local States in String Diagrams. Springer International Publishing, Cham, 334--348."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.47"},{"volume-title":"Foundations of Software Science and Computation Structures","author":"Miquey \u00c9tienne","key":"e_1_3_2_1_24_1","unstructured":"\u00c9tienne Miquey and Hugo Herbelin . 2018. Realizability Interpretation and Normalization of Typed Call-by-Need \u03bb-calculus with Control . In Foundations of Software Science and Computation Structures , Christel Baier and Ugo Dal Lago (Eds.). Springer International Publishing , Cham , 276--292. https:\/\/doi.org\/10.1007\/978-3-319-89366-2_15 10.1007\/978-3-319-89366-2_15 \u00c9tienne Miquey and Hugo Herbelin. 2018. Realizability Interpretation and Normalization of Typed Call-by-Need \u03bb-calculus with Control. In Foundations of Software Science and Computation Structures, Christel Baier and Ugo Dal Lago (Eds.). Springer International Publishing, Cham, 276--292. https:\/\/doi.org\/10.1007\/978-3-319-89366-2_15"},{"key":"e_1_3_2_1_25_1","unstructured":"Ieke Moerdijk and Jaap van Oosten. 2007. Topos Theory. (2007). http:\/\/www.staff.science.uu.nl\/~ooste110\/syllabi\/toposmoeder.pdf  Ieke Moerdijk and Jaap van Oosten. 2007. Topos Theory. (2007). http:\/\/www.staff.science.uu.nl\/~ooste110\/syllabi\/toposmoeder.pdf"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019945"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275652"},{"volume-title":"Notions of Computation Determine Monads","author":"Plotkin Gordon","key":"e_1_3_2_1_29_1","unstructured":"Gordon Plotkin and John Power . 2002. Notions of Computation Determine Monads . Springer Berlin Heidelberg , Berlin, Heidelberg , 342--356. Gordon Plotkin and John Power. 2002. Notions of Computation Determine Monads. Springer Berlin Heidelberg, Berlin, Heidelberg, 342--356."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002712"},{"key":"e_1_3_2_1_32_1","volume-title":"Coq. Proc. ACM Program. Lang. 4, POPL, Article Article 8 (Dec.","author":"Sozeau Matthieu","year":"2019","unstructured":"Matthieu Sozeau , Simon Boulier , Yannick Forster , Nicolas Tabareau , and Th\u00e9o Winterhalter . 2019 . Coq Coq Correct! Verification of Type Checking and Erasure for Coq , in Coq. Proc. ACM Program. Lang. 4, POPL, Article Article 8 (Dec. 2019), 28 pages. https:\/\/doi.org\/10.1145\/3371076 10.1145\/3371076 Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Th\u00e9o Winterhalter. 2019. Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq. Proc. ACM Program. Lang. 4, POPL, Article Article 8 (Dec. 2019), 28 pages. https:\/\/doi.org\/10.1145\/3371076"},{"key":"e_1_3_2_1_33_1","volume-title":"Jr.","author":"Sussman Gerald J.","year":"1975","unstructured":"Gerald J. Sussman and Guy L . Steele , Jr. 1975 . An Interpreter for Extended Lambda Calculus. Technical Report. Massachusetts Institute of Technology , Cambridge, MA, USA. Gerald J. Sussman and Guy L. Steele, Jr. 1975. An Interpreter for Extended Lambda Calculus. Technical Report. Massachusetts Institute of Technology, Cambridge, MA, USA."}],"event":{"name":"LICS '20: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"],"location":"Saarbr\u00fccken Germany","acronym":"LICS '20"},"container-title":["Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394792","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394792","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:35Z","timestamp":1750197755000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394792"}},"subtitle":["Continuation-and-environment-passing style translations"],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":32,"alternative-id":["10.1145\/3373718.3394792","10.1145\/3373718"],"URL":"https:\/\/doi.org\/10.1145\/3373718.3394792","relation":{},"subject":[],"published":{"date-parts":[[2020,7,8]]},"assertion":[{"value":"2020-07-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}