{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:52:13Z","timestamp":1773193933778,"version":"3.50.1"},"reference-count":61,"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\/4.0\/"}],"funder":[{"name":"DARPA \/ AFRL","award":["FA8750-10-C-0237, HR0011-18-C-0016, FA8650-18-C-7809"],"award-info":[{"award-number":["FA8750-10-C-0237, HR0011-18-C-0016, FA8650-18-C-7809"]}]},{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","award":["789108"],"award-info":[{"award-number":["789108"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K008528\/1"],"award-info":[{"award-number":["EP\/K008528\/1"]}],"id":[{"id":"10.13039\/501100000266","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":[[2019,1,2]]},"abstract":"<jats:p>Architecture specifications notionally define the fundamental interface between hardware and software: the envelope of allowed behaviour for processor implementations, and the basic assumptions for software development and verification. But in practice, they are typically prose and pseudocode documents, not rigorous or executable artifacts, leaving software and verification on shaky ground.<\/jats:p>\n          <jats:p>In this paper, we present rigorous semantic models for the sequential behaviour of large parts of the mainstream ARMv8-A, RISC-V, and MIPS architectures, and the research CHERI-MIPS architecture, that are complete enough to boot operating systems, variously Linux, FreeBSD, or seL4. Our ARMv8-A models are automatically translated from authoritative ARM-internal definitions, and (in one variant) tested against the ARM Architecture Validation Suite.<\/jats:p>\n          <jats:p>We do this using a custom language for ISA semantics, Sail, with a lightweight dependent type system, that supports automatic generation of emulator code in C and OCaml, and automatic generation of proof-assistant definitions for Isabelle, HOL4, and (currently only for MIPS) Coq. We use the former for validation, and to assess specification coverage. To demonstrate the usability of the latter, we prove (in Isabelle) correctness of a purely functional characterisation of ARMv8-A address translation. We moreover integrate the RISC-V model into the RMEM tool for (user-mode) relaxed-memory concurrency exploration. We prove (on paper) the soundness of the core Sail type system.<\/jats:p>\n          <jats:p>We thereby take a big step towards making the architectural abstraction actually well-defined, establishing foundations for verification and reasoning.<\/jats:p>","DOI":"10.1145\/3290384","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":100,"title":["ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS"],"prefix":"10.1145","volume":"3","author":[{"given":"Alasdair","family":"Armstrong","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Thomas","family":"Bauereiss","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Brian","family":"Campbell","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}]},{"given":"Alastair","family":"Reid","sequence":"additional","affiliation":[{"name":"ARM, UK"}]},{"given":"Kathryn E.","family":"Gray","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Robert M.","family":"Norton","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Prashanth","family":"Mundkur","sequence":"additional","affiliation":[{"name":"SRI International, USA"}]},{"given":"Mark","family":"Wassell","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Jon","family":"French","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Christopher","family":"Pulte","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Shaked","family":"Flur","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Ian","family":"Stark","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}]},{"given":"Neel","family":"Krishnaswami","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2017. The gem5 Simulator. http:\/\/gem5.org .  2017. The gem5 Simulator. http:\/\/gem5.org ."},{"key":"e_1_2_2_2_1","unstructured":"2017. QEMU: the FAST! processor emulator. https:\/\/www.qemu.org\/ .  2017. QEMU: the FAST! processor emulator. https:\/\/www.qemu.org\/ ."},{"key":"e_1_2_2_3_1","volume-title":"The RISC-V Instruction Set Manual. Volume I: User-Level ISA","unstructured":"2017. The RISC-V Instruction Set Manual. Volume I: User-Level ISA ; Volume II : Privileged Architecture . https:\/\/riscv.org\/ specifications\/ . 236 pages. 2017. The RISC-V Instruction Set Manual. Volume I: User-Level ISA; Volume II: Privileged Architecture. https:\/\/riscv.org\/ specifications\/ . 236 pages."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_2_6_1","volume-title":"Foundational and Practical Aspects of Resource Analysis -Third International Workshop, FOPARA 2013","author":"Amadio Roberto M.","year":"2013","unstructured":"Roberto M. Amadio , Nicholas Ayache , Fran\u00e7ois Bobot , Jaap Boender , Brian Campbell , Ilias Garnier , Antoine Madet , James McKinna , Dominic P. Mulligan , Mauro Piccolo , Randy Pollack , Yann R\u00e9gis-Gianas , Claudio Sacerdoti Coen , Ian Stark , and Paolo Tranquilli . 2013 . Certified Complexity (CerCo) . In Foundational and Practical Aspects of Resource Analysis -Third International Workshop, FOPARA 2013 , Bertinoro, Italy , August 29-31, 2013, Revised Selected Papers. 1\u201318. Roberto M. Amadio, Nicholas Ayache, Fran\u00e7ois Bobot, Jaap Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic P. Mulligan, Mauro Piccolo, Randy Pollack, Yann R\u00e9gis-Gianas, Claudio Sacerdoti Coen, Ian Stark, and Paolo Tranquilli. 2013. Certified Complexity (CerCo). In Foundational and Practical Aspects of Resource Analysis -Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013, Revised Selected Papers. 1\u201318."},{"key":"e_1_2_2_7_1","unstructured":"Andrew W. Appel Lennart Beringer Robert Dockins Josiah Dodds Aquinas Hobor Gordon Stewart and Qinxiang Cao. 2017. Verified Software Toolchain. http:\/\/vst.cs.princeton.edu\/download\/ .  Andrew W. Appel Lennart Beringer Robert Dockins Josiah Dodds Aquinas Hobor Gordon Stewart and Qinxiang Cao. 2017. Verified Software Toolchain. http:\/\/vst.cs.princeton.edu\/download\/ ."},{"key":"e_1_2_2_8_1","unstructured":"ARM. 2017. ARM Architecture Reference Manual. ARMv8 for ARMv8-A architecture profile. v8.2 Beta. 6354 pages.  ARM. 2017. ARM Architecture Reference Manual. ARMv8 for ARMv8-A architecture profile. v8.2 Beta. 6354 pages."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuCNC.2016.7561034"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328487"},{"key":"e_1_2_2_11_1","volume-title":"CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.)","volume":"6806","author":"Brumley David","unstructured":"David Brumley , Ivan Jager , Thanassis Avgerinos , and Edward J. Schwartz . 2011. BAP: A Binary Analysis Platform. In Computer Aided Verification - 23rd International Conference , CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.) , Vol. 6806 . Springer, 463\u2013469. David Brumley, Ivan Jager, Thanassis Avgerinos, and Edward J. Schwartz. 2011. BAP: A Binary Analysis Platform. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), Vol. 6806. Springer, 463\u2013469."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110268"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706346"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009839"},{"key":"e_1_2_2_22_1","volume-title":"ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings. 338\u2013344","author":"Fox Anthony C. J.","year":"2012","unstructured":"Anthony C. J. Fox . 2012 . Directions in ISA Specification. In Interactive Theorem Proving \u2013 Third International Conference , ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings. 338\u2013344 . Anthony C. J. Fox. 2012. Directions in ISA Specification. In Interactive Theorem Proving \u2013 Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings. 338\u2013344."},{"key":"e_1_2_2_23_1","volume-title":"ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, Christian Urban and Xingyuan Zhang (Eds.)","volume":"9236","author":"Fox Anthony C. J.","year":"2015","unstructured":"Anthony C. J. Fox . 2015 . Improved Tool Support for Machine-Code Decompilation in HOL4. In Interactive Theorem Proving -6th International Conference , ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, Christian Urban and Xingyuan Zhang (Eds.) , Vol. 9236 . Springer, 187\u2013202. Anthony C. J. Fox. 2015. Improved Tool Support for Machine-Code Decompilation in HOL4. In Interactive Theorem Proving -6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, Christian Urban and Xingyuan Zhang (Eds.), Vol. 9236. Springer, 187\u2013202."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018621"},{"key":"e_1_2_2_26_1","doi-asserted-by":"crossref","unstructured":"Shilpi Goel Warren A. Hunt  Jr. and Matt Kaufmann. 2017. Engineering a Formal Executable x86 ISA Simulator for Software Verification. In Provably Correct Systems. 173\u2013209.  Shilpi Goel Warren A. Hunt Jr. and Matt Kaufmann. 2017. Engineering a Formal Executable x86 ISA Simulator for Software Verification. In Provably Correct Systems. 173\u2013209.","DOI":"10.1007\/978-3-319-48628-4_8"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_2_29_1","volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan (Newman) Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016 , Savannah, GA, USA , November 2-4, 2016. 653\u2013669. https: \/\/www.usenix.org\/conference\/osdi16\/technical- sessions\/presentation\/gu Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016. 653\u2013669. https: \/\/www.usenix.org\/conference\/osdi16\/technical- sessions\/presentation\/gu"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-160558"},{"key":"e_1_2_2_31_1","unstructured":"Intel Corporation. 2017. Intel 64 and IA-32 Architectures Software Developer\u2019s Manual. Combined Volumes: 1 2A 2B 2C 2D 3A 3B 3C 3D and 4. https:\/\/software.intel.com\/en- us\/articles\/intel- sdm . 325462-063US. 4744 pages.  Intel Corporation. 2017. Intel 64 and IA-32 Architectures Software Developer\u2019s Manual. Combined Volumes: 1 2A 2B 2C 2D 3A 3B 3C 3D and 4. https:\/\/software.intel.com\/en- us\/articles\/intel- sdm . 325462-063US. 4744 pages."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429105"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25942-0_7"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505897"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_2_40_1","unstructured":"Xavier Leroy et al. 2017. CompCert 3.1. http:\/\/compcert.inria.fr\/ .  Xavier Leroy et al. 2017. CompCert 3.1. http:\/\/compcert.inria.fr\/ ."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2450136.2450139"},{"key":"e_1_2_2_42_1","unstructured":"Prabhat Misra and Nikil Dutt (Eds.). 2008. Processor Description Languages. Morgan Kaufmann.   Prabhat Misra and Nikil Dutt (Eds.). 2008. Processor Description Languages. Morgan Kaufmann."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254111"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250746"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/125826.125848"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/3077629.3077658"},{"key":"e_1_2_2_50_1","unstructured":"Alastair Reid. 2017. ARM Releases Machine Readable Architecture Specification. https:\/\/alastairreid.github.io\/ ARM- v8a- xml- release\/ .  Alastair Reid. 2017. ARM Releases Machine Readable Architecture Specification. https:\/\/alastairreid.github.io\/ ARM- v8a- xml- release\/ ."},{"key":"e_1_2_2_51_1","volume-title":"CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II (Lecture Notes in Computer Science), Swarat Chaudhuri and Azadeh Farzan (Eds.)","volume":"9780","author":"Reid Alastair","year":"2016","unstructured":"Alastair Reid , Rick Chen , Anastasios Deligiannis , David Gilday , David Hoyes , Will Keen , Ashan Pathirane , Owen Shepherd , Peter Vrabel , and Ali Zaidi . 2016 . End-to-End Verification of Processors with ISA-Formal. In Computer Aided Verification - 28th International Conference , CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II (Lecture Notes in Computer Science), Swarat Chaudhuri and Azadeh Farzan (Eds.) , Vol. 9780 . Springer, 42\u201358. Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Zaidi. 2016. End-to-End Verification of Processors with ISA-Formal. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II (Lecture Notes in Computer Science), Swarat Chaudhuri and Azadeh Farzan (Eds.), Vol. 9780. Springer, 42\u201358."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_2_2_55_1","unstructured":"Xiaomu Shi. 2013. Certification of an Instruction Set Simulator. Theses. Universit\u00e9 de Grenoble. https:\/\/tel.archives- ouvertes. fr\/tel- 00937524  Xiaomu Shi. 2013. Certification of an Instruction Set Simulator. Theses. Universit\u00e9 de Grenoble. https:\/\/tel.archives- ouvertes. fr\/tel- 00937524"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.17"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167092"},{"key":"e_1_2_2_58_1","volume-title":"ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings (Lecture Notes in Computer Science), Jeremy Avigad and Assia Mahboubi (Eds.)","volume":"10895","author":"Syeda Hira Taqdees","year":"2018","unstructured":"Hira Taqdees Syeda and Gerwin Klein . 2018 . Program Verification in the Presence of Cached Address Translation. In Interactive Theorem Proving - 9th International Conference , ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings (Lecture Notes in Computer Science), Jeremy Avigad and Assia Mahboubi (Eds.) , Vol. 10895 . Springer, 542\u2013559. Hira Taqdees Syeda and Gerwin Klein. 2018. Program Verification in the Presence of Cached Address Translation. In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings (Lecture Notes in Computer Science), Jeremy Avigad and Assia Mahboubi (Eds.), Vol. 10895. Springer, 542\u2013559."},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951924"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"},{"key":"e_1_2_2_62_1","volume-title":"symposium on Computer architecture. IEEE Press","author":"Woodruff Jonathan","year":"2014","unstructured":"Jonathan Woodruff , Robert N.M. Watson , David Chisnall , Simon W. Moore , Jonathan Anderson , Brooks Davis , Ben Laurie , Peter G. Neumann , Robert Norton , and Michael Roe . 2014 . The CHERI capability model: revisiting RISC in an age of risk. In ISCA \u201914: Proceeding of the 41st annual international symposium on Computer architecture. IEEE Press , Piscataway, NJ, USA, 457\u2013468. Jonathan Woodruff, Robert N.M. Watson, David Chisnall, Simon W. Moore, Jonathan Anderson, Brooks Davis, Ben Laurie, Peter G. Neumann, Robert Norton, and Michael Roe. 2014. The CHERI capability model: revisiting RISC in an age of risk. In ISCA \u201914: Proceeding of the 41st annual international symposium on Computer architecture. IEEE Press, Piscataway, NJ, USA, 457\u2013468."},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006216"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290384","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290384","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\/3290384"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":61,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290384"],"URL":"https:\/\/doi.org\/10.1145\/3290384","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"}}]}}