{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:45Z","timestamp":1779836745672,"version":"3.53.1"},"reference-count":47,"publisher":"Cambridge University Press (CUP)","issue":"4-5","license":[{"start":{"date-parts":[[2012,8,15]],"date-time":"2012-08-15T00:00:00Z","timestamp":1344988800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2012,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Reasoning about program equivalence is one of the oldest problems in semantics. In recent years, useful techniques have been developed, based on bisimulations and logical relations, for reasoning about equivalence in the setting of increasingly realistic languages\u2014languages nearly as complex as ML or Haskell. Much of the recent work in this direction has considered the interesting representation independence principles\n                    <jats:italic>enabled<\/jats:italic>\n                    by the use of local state, but it is also important to understand the principles that powerful features like higher-order state and control effects\n                    <jats:italic>disable<\/jats:italic>\n                    . This latter topic has been broached extensively within the framework of game semantics, resulting in what Abramsky dubbed the \u201csemantic cube\u201d: fully abstract game-semantic characterizations of various axes in the design space of ML-like languages. But when it comes to reasoning about many actual examples, game semantics does not yet supply a useful technique for proving equivalences.\n                  <\/jats:p>\n                  <jats:p>\n                    In this paper, we marry the aspirations of the semantic cube to the powerful proof method of\n                    <jats:italic>step-indexed Kripke logical relations<\/jats:italic>\n                    . Building on recent work of Ahmed\n                    <jats:italic>et al<\/jats:italic>\n                    . (2009), we define the first fully abstract logical relation for an ML-like language with recursive types, abstract types, general references and call\/cc. We then show how, under orthogonal restrictions to the expressive power of our language\u2014namely, the restriction to first-order state and\/or the removal of call\/cc\u2014we can enhance the proving power of our possible-worlds model in correspondingly orthogonal ways, and we demonstrate this proving power on a range of interesting examples. Central to our story is the use of\n                    <jats:italic>state transition systems<\/jats:italic>\n                    to model the way in which properties of local state evolve over time.\n                  <\/jats:p>","DOI":"10.1017\/s095679681200024x","type":"journal-article","created":{"date-parts":[[2012,8,15]],"date-time":"2012-08-15T08:45:18Z","timestamp":1345020318000},"page":"477-528","source":"Crossref","is-referenced-by-count":49,"title":["The impact of higher-order state and control effects on local relational reasoning"],"prefix":"10.1017","volume":"22","author":[{"given":"DEREK","family":"DREYER","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"GEORG","family":"NEIS","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"LARS","family":"BIRKEDAL","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2012,8,15]]},"reference":[{"key":"S095679681200024X_ref33","doi-asserted-by":"crossref","unstructured":"Pilkiewicz A. & Pottier F. (2011) The essence of monotonic state. Proceedings of ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI).","DOI":"10.1145\/1929553.1929565"},{"key":"S095679681200024X_ref15","doi-asserted-by":"crossref","unstructured":"Hur C.-K. & Dreyer D. (2011) A Kripke logical relation between ML and assembly. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","DOI":"10.1145\/1926385.1926402"},{"key":"S095679681200024X_ref23","unstructured":"Laird J. (1997) Full abstraction for functional languages with control. Proceedings of IEEE Symposium on Logic in Computer Science (LICS)."},{"key":"S095679681200024X_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"S095679681200024X_ref38","unstructured":"Pottier F. (2009) Generalizing the Higher-Order Frame and Anti-Frame Rules. Unpublished."},{"key":"S095679681200024X_ref42","doi-asserted-by":"crossref","unstructured":"Schwinghammer J. , Yang H. , Birkedal L. , Pottier F. & Reus B. (2010) A semantic foundation for hidden state. Proceedings of Foundations of Software Science and Computation Structures (FOSSACS).","DOI":"10.1007\/978-3-642-12032-9_2"},{"key":"S095679681200024X_ref18","doi-asserted-by":"crossref","unstructured":"Johann P. , Simpson A. & Voigtl\u00e4nder J. (2010) A generic operational metatheory for algebraic effects. Proceedings of IEEE Symposium on Logic in Computer Science (LICS).","DOI":"10.1109\/LICS.2010.29"},{"key":"S095679681200024X_ref6","doi-asserted-by":"crossref","unstructured":"Benton N. & Tabareau N. (2009) Compiling functional types to relational specifications for low level imperative code. Proceedings of ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI).","DOI":"10.1145\/1481861.1481864"},{"key":"S095679681200024X_ref30","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1109\/LICS.2011.31","volume-title":"26th Annual IEEE Symposium on Logic in Computer Science","author":"Murawski","year":"2011"},{"key":"S095679681200024X_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1890002"},{"key":"S095679681200024X_ref10","unstructured":"Dreyer D. , Neis G. & Birkedal L. (2012) The Impact of Higher-Order State and Control Effects on Local Relational Reasoning (Technical Appendix). Tech. Rep. MPI-SWS-2012-001. Max Planck Institute for Software Systems (MPI-SWS), Germany. Available at: http:\/\/www.mpi-sws.org\/tr\/2012-001.pdf."},{"key":"S095679681200024X_ref28","unstructured":"Morris J. H. Jr. (1968) Lambda-Calculus Models of Programming Languages. PhD. thesis. Massachusetts Institute of Technology."},{"key":"S095679681200024X_ref8","unstructured":"Bohr N. (2007) Advances in Reasoning Principles for Contextual Equivalence and Termination. PhD. thesis. IT University of Copenhagen."},{"key":"S095679681200024X_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90047-7"},{"key":"S095679681200024X_ref39","unstructured":"Reddy U. S. & Dunphy B. P. (2011) An automata-theoretic model of objects. Proceedings of International Workshop on Foundations of Object-Oriented Languages (FOOL)."},{"key":"S095679681200024X_ref9","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"S095679681200024X_ref37","doi-asserted-by":"crossref","unstructured":"Pottier F. (2008) Hiding local state in direct style: A higher-order anti-frame rule. Proceedings of IEEE Symposium on Logic in Computer Science (LICS).","DOI":"10.1109\/LICS.2008.16"},{"key":"S095679681200024X_ref21","doi-asserted-by":"crossref","unstructured":"Koutavas V. & Wand M. (2006) Small bisimulations for reasoning about higher-order imperative programs. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","DOI":"10.1145\/1111037.1111050"},{"key":"S095679681200024X_ref47","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:2)2008"},{"key":"S095679681200024X_ref46","doi-asserted-by":"crossref","unstructured":"Thielecke H. (2000) On exceptions versus continuations in the presence of state. Proceedings of European Symposium on Programming (ESOP).","DOI":"10.1007\/3-540-46425-5_26"},{"key":"S095679681200024X_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"S095679681200024X_ref7","doi-asserted-by":"crossref","unstructured":"Birkedal L. , M\u00f8gelberg R. , Schwinghammer J. & St\u00f8vring K. (January 2011) First steps in synthetic guarded domain theory: Step-indexing in the topos of trees. Proceedings of IEEE Symposium on Logic in Computer Science (LICS).","DOI":"10.1109\/LICS.2011.16"},{"key":"S095679681200024X_ref25","unstructured":"Lassen S. B. & Levy P. B. (2007) Typed normal form bisimulation. Proceedings of Conference on Computer Science Logic (CSL)."},{"key":"S095679681200024X_ref43","doi-asserted-by":"crossref","unstructured":"St\u00f8vring K. & Lassen S. B. (2007) A complete, co-inductive syntactic theory of sequential control and state. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","DOI":"10.1145\/1190216.1190244"},{"key":"S095679681200024X_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/1284320.1284325"},{"key":"S095679681200024X_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.12.036"},{"key":"S095679681200024X_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.022"},{"key":"S095679681200024X_ref5","doi-asserted-by":"crossref","unstructured":"Benton N. & Hur C.-K. (2009) Biorthogonality, step-indexing and compiler correctness. Proceedings of ACM SIGPLAN International Conference on Functional Programming (ICFP).","DOI":"10.1145\/1596550.1596567"},{"key":"S095679681200024X_ref35","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pitts","year":"2005"},{"key":"S095679681200024X_ref14","doi-asserted-by":"crossref","unstructured":"Ghica Dan R. & McCusker G. (2000) Reasoning about Idealized Algol using regular languages. Proceedings of International Colloquium on Automata, Languages and Programming (ICALP).","DOI":"10.1007\/3-540-45022-X_10"},{"key":"S095679681200024X_ref32","unstructured":"O'Hearn P. & Reddy U. (1995) Objects, interference, and the Yoneda embedding. Proceedings of Conference on the Mathematical Foundations of Programming Semantics (MFPS)."},{"key":"S095679681200024X_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004409"},{"key":"S095679681200024X_ref20","unstructured":"Koutavas V. & Lassen S. (February 2008) Fun with Fully Abstract Operational Game Semantics for General References. Unpublished."},{"key":"S095679681200024X_ref24","unstructured":"Laird J. (2007) A fully abstract trace semantics for general references. Proceedings of International Colloquium on Automata, Languages and Programming (ICALP)."},{"key":"S095679681200024X_ref36","unstructured":"Pitts A. & Stark I. (1998) Operational reasoning for functions with local state. Proceedings of International Workshop on Higher Order Operational Techniques in Semantics (HOOTS)."},{"key":"S095679681200024X_ref11","doi-asserted-by":"crossref","unstructured":"Dreyer D. , Neis G. , Rossberg A. & Birkedal L. (2010) A relational modal logic for higher-order stateful ADTs. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","DOI":"10.1145\/1706299.1706323"},{"key":"S095679681200024X_ref34","doi-asserted-by":"crossref","unstructured":"Pitts A. M. (1996) Reasoning about local variables with operationally-based logical relations. Proceedings of IEEE Symposium on Logic in Computer Science (LICS).","DOI":"10.1007\/978-1-4757-3851-3_7"},{"key":"S095679681200024X_ref2","unstructured":"Ahmed A. (2004) Semantics of Types for Mutable State. PhD. thesis. Princeton University."},{"key":"S095679681200024X_ref27","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000125"},{"key":"S095679681200024X_ref26","doi-asserted-by":"crossref","unstructured":"Lassen S. B. & Levy P. B. (2008) Typed normal form bisimulation for parametric polymorphism. Proceedings of IEEE Symposium on Logic in Computer Science (LICS).","DOI":"10.1109\/LICS.2008.26"},{"key":"S095679681200024X_ref1","unstructured":"Abramsky S. , Honda K. & McCusker G. (1998) A fully abstract game semantics for general references. Proceedings of IEEE Symposium on Logic in Computer Science (LICS)."},{"key":"S095679681200024X_ref13","doi-asserted-by":"crossref","unstructured":"Friedman D. & Haynes C. (1985) Constraining control. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","DOI":"10.1145\/318593.318654"},{"key":"S095679681200024X_ref16","doi-asserted-by":"crossref","unstructured":"Hur C.-K. , Dreyer D. , Neis G. & Vafeiadis V. (2012) The marriage of bisimulations and Kripke logical relations. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","DOI":"10.1145\/2103656.2103666"},{"key":"S095679681200024X_ref44","doi-asserted-by":"crossref","unstructured":"Sumii E. (2009) A complete characterization of observational equivalence in polymorphic \u03bb-calculus with general references. Proceedings of Conference on Computer Science Logic (CSL).","DOI":"10.1007\/978-3-642-04027-6_33"},{"key":"S095679681200024X_ref3","doi-asserted-by":"crossref","unstructured":"Ahmed A. , Dreyer D. & Rossberg A. (2009) State-dependent representation independence. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","DOI":"10.1145\/1480881.1480925"},{"key":"S095679681200024X_ref19","first-page":"63","article-title":"The impact of seq on free theorems-based program transformations","volume":"69","author":"Johann","year":"2006","journal-title":"Fundam. Inform."},{"key":"S095679681200024X_ref41","doi-asserted-by":"crossref","unstructured":"Schwinghammer J. , Birkedal L. , Pottier F. , Reus B. , St\u00f8vring K. & Yang H. (2012) A step-indexed Kripke model of hidden state. In Mathematical Structures in Computer Science. To appear.","DOI":"10.1017\/S0960129512000035"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S095679681200024X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:27Z","timestamp":1779834987000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S095679681200024X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,15]]},"references-count":47,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2012,9]]}},"alternative-id":["S095679681200024X"],"URL":"https:\/\/doi.org\/10.1017\/s095679681200024x","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8,15]]}}}