{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T08:00:10Z","timestamp":1790928010066,"version":"4.1.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["REMS EP\/K008528\/1"],"award-info":[{"award-number":["REMS EP\/K008528\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"ANR","award":["AJACS ANR-14-CE28-0008, CISC ANR-17-CE25-0014-01"],"award-info":[{"award-number":["AJACS ANR-14-CE28-0008, CISC ANR-17-CE25-0014-01"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>\n            The development of mechanised language specification based on structured operational semantics, with applications to verified compilers and sound program analysis, requires huge effort. General theory and frameworks have been proposed to help with this effort. However, none of this work provides a systematic way of developing concrete and abstract semantics, connected together by a general consistency result. We introduce a\n            <jats:italic>skeletal semantics<\/jats:italic>\n            of a language, where each skeleton describes the complete semantic behaviour of a language construct. We define a general notion of\n            <jats:italic>interpretation<\/jats:italic>\n            , which provides a systematic and language-independent way of deriving semantic judgements from the skeletal semantics. We explore four generic interpretations: a simple well-formedness interpretation; a concrete interpretation; an abstract interpretation; and a constraint generator for flow-sensitive analysis. We prove general\n            <jats:italic>consistency results<\/jats:italic>\n            between interpretations, depending only on simple language-dependent lemmas. We illustrate our ideas using a simple While language.\n          <\/jats:p>","DOI":"10.1145\/3290357","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["Skeletal semantics and their interpretations"],"prefix":"10.1145","volume":"3","author":[{"given":"Martin","family":"Bodin","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philippa","family":"Gardner","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alan","family":"Schmitt","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693174"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.004"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_3"},{"key":"e_1_2_2_6_1","volume-title":"Transactions on","author":"Churchill Martin"},{"key":"e_1_2_2_7_1","volume-title":"Calculational System Design","author":"Cousot Patrick"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984027"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_2_11_1","volume-title":"ECMAScript 2018 Language Specification (ECMA-262","author":"ECMA.","year":"2018","edition":"9"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103663"},{"key":"e_1_2_2_13_1","volume-title":"Proc. of the Symposium on Logic in Computer Science (LICS \u201987)","author":"Harper Robert"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"e_1_2_2_15_1","volume-title":"Iris from the Ground Up. Submitted to JFP","author":"Jung Ralf","year":"2017"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236767"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00869-1"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_2_20_1","volume-title":"Gunter","author":"Li Liyi","year":"2018"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_22"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_23"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Peter D. Mosses. 1992. Action Semantics. Cambridge University Press.   Peter D. Mosses. 1992. Action Semantics. Cambridge University Press.","DOI":"10.1017\/CBO9780511569869"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_2_2_25_1","volume-title":"Principles of Program Analysis","author":"Nielson Flemming"},{"key":"e_1_2_2_27_1","volume-title":"Proc. of 17th European Symposium on Programming, ESOP 2008. Springer LNCS","volume":"4960","author":"Owens Scott","year":"2008"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/200994.201001"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753634"},{"key":"e_1_2_2_31_1","first-page":"1","article-title":"Matching Logic","volume":"13","author":"Ro\u015fu Grigore","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/647163.717672"},{"key":"e_1_2_2_34_1","volume-title":"Abstract Interpretation in the Operational Semantics Hierarchy. BRICS Report Series 4, 2","author":"Schmidt David A.","year":"1997"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/646912.710955"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/788019.788864"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.137.6"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863553"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995400"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290357","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290357","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290357"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":38,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290357"],"URL":"https:\/\/doi.org\/10.1145\/3290357","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}