{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T05:19:16Z","timestamp":1768713556563,"version":"3.49.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000288","name":"Royal Society","doi-asserted-by":"publisher","award":["RSWF\\R1\\22100"],"award-info":[{"award-number":["RSWF\\R1\\22100"]}],"id":[{"id":"10.13039\/501100000288","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            Rewriting is a versatile and powerful technique used in many domains.\n            <jats:italic toggle=\"yes\">Strategic rewriting<\/jats:italic>\n            allows programmers to control the application of rewrite rules by composing individual rewrite rules into complex rewrite strategies. These strategies are semantically complex, as they may be nondeterministic, they may raise errors that trigger backtracking, and they may not terminate.\n          <\/jats:p>\n          <jats:p>Given such semantic complexity, it is necessary to establish a formal understanding of rewrite strategies and to enable reasoning about them in order to answer questions like: How do we know that a rewrite strategy terminates? How do we know that a rewrite strategy does not fail because we compose two incompatible rewrites? How do we know that a desired property holds after applying a rewrite strategy?<\/jats:p>\n          <jats:p>\n            In this paper, we introduce Shoggoth: a formal foundation for understanding, analysing and reasoning about strategic rewriting that is capable of answering these questions. We provide a denotational semantics of System S, a core language for strategic rewriting, and prove its equivalence to our big-step operational semantics, which extends existing work by explicitly accounting for divergence. We further define a\n            <jats:italic toggle=\"yes\">location-based weakest precondition calculus<\/jats:italic>\n            to enable formal reasoning about rewriting strategies, and we prove this calculus sound with respect to the denotational semantics. We show how this calculus can be used in practice to reason about properties of rewriting strategies, including termination, that they are well-composed, and that desired postconditions hold. The semantics and calculus are formalised in Isabelle\/HOL and all proofs are mechanised.\n          <\/jats:p>","DOI":"10.1145\/3633211","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"61-89","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Shoggoth: A Formal Foundation for Strategic Rewriting"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4825-2023","authenticated-orcid":false,"given":"Xueying","family":"Qin","sequence":"first","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2765-4269","authenticated-orcid":false,"given":"Liam","family":"O\u2019Connor","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4712-7423","authenticated-orcid":false,"given":"Rob","family":"van Glabbeek","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"},{"name":"UNSW, Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2141-5868","authenticated-orcid":false,"given":"Peter","family":"H\u00f6fner","sequence":"additional","affiliation":[{"name":"Australian National University, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2071-0929","authenticated-orcid":false,"given":"Ohad","family":"Kammar","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5048-0741","authenticated-orcid":false,"given":"Michel","family":"Steuwer","sequence":"additional","affiliation":[{"name":"TU Berlin, Germany"},{"name":"University of Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129522000330"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56596-5_30"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00032-5"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.11.003"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1244381.1244385"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80003-6"},{"key":"e_1_3_1_11_1","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/978-3-319-89366-2_4","volume-title":"Foundations of Software Science and Computation Structures","author":"Campos Marco Devesas","year":"2018","unstructured":"Marco Devesas Campos and Paul Blain Levy. 2018. A Syntactic View of Computational Adequacy. In Foundations of Software Science and Computation Structures, Christel Baier and Ugo Dal Lago (Eds.). Springer International Publishing, Cham, 71\u201387."},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"e_1_3_1_15_1","unstructured":"Rongxiao Fu Ornela Dardha and Michel Steuwer. 2023. Traced Types for Safe Strategic Rewriting. arXiv:2304.14154 [cs.PL]"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.33"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408974"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3580371"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09526-8_8"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2011.04.005"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.29"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599423"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00283-X"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.EVCS.2023.16"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151646"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782610"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00028-0"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190240"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.11.006"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/570186.570187"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.10.015"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.12.004"},{"key":"e_1_3_1_36_1","volume-title":"Programming from specifications","author":"Morgan Carroll","year":"1994","unstructured":"Carroll Morgan. 1994. Programming from specifications, 2nd Edition. Prentice Hall.","edition":"2"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_1_38_1","first-page":"1","volume-title":"Foundations of Software Science and Computation Structures","author":"Plotkin Gordon","year":"2001","unstructured":"Gordon Plotkin and John Power. 2001. Adequacy for Algebraic Effects. In Foundations of Software Science and Computation Structures, Furio Honsell and Marino Miculan (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1\u201324."},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205035"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","unstructured":"Xueying Qin Liam O\u2019Connor Rob van Glabbeek Peter H\u00f6fner Ohad Kammar and Michel Steuwer. 2023. Artifact for Shoggoth - A Formal Foundation for Strategic Rewriting. https:\/\/doi.org\/10.5281\/zenodo.10125602 10.5281\/zenodo.10125602","DOI":"10.5281\/zenodo.10125602"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2003.12.005"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3426425.3426928"},{"key":"e_1_3_1_43_1","unstructured":"Matthieu Sozeau. 2014. Proof-relevant rewriting strategies in Coq. In At Coq Workshop. https:\/\/www.irif.fr\/~letouzey\/types2014\/abstract-13.pdf"},{"key":"e_1_3_1_44_1","volume-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory","author":"Stoy J.E.","year":"1985","unstructured":"J.E. Stoy. 1985. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press. https:\/\/books.google.co.uk\/books?id=jM0mAAAAMAAJ"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341707"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45127-7_27"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289425"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80027-1"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2014.100"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_21"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.03.006"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3633211","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3633211","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:06:26Z","timestamp":1751659586000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3633211"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":50,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3633211"],"URL":"https:\/\/doi.org\/10.1145\/3633211","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}