{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T09:47:03Z","timestamp":1774000023557,"version":"3.50.1"},"reference-count":102,"publisher":"Association for Computing Machinery (ACM)","issue":"1","funder":[{"name":"ASPIRE faculty awards"},{"name":"Birkedal, Pichon-Pharabod, and Sewell"},{"name":"European Research Council","award":["789108"],"award-info":[{"award-number":["789108"]}]},{"name":"Villum Investigator","award":["25804"],"award-info":[{"award-number":["25804"]}]},{"name":"Innovate UK project Digital Security by Design (DSbD) Technology Platform Prototype","award":["105694"],"award-info":[{"award-number":["105694"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2026,3,31]]},"abstract":"<jats:p>Very relaxed concurrency memory models, like those of the Arm-A, RISC-V and IBM Power hardware architectures, underpin much of computing but break a fundamental intuition about programs, namely that syntactic program order and the reads-from relation always both induce order in the execution. Instead, out-of-order execution is allowed except where prevented by certain pairwise dependencies, barriers, or other synchronisation. This means that there is no notion of the \u2018current\u2019 state of the program, making it challenging to design (and prove sound) syntax-directed, modular reasoning methods like Hoare logics, as usable resources cannot implicitly flow from one program point to the next.<\/jats:p>\n                  <jats:p>We present AxSL, a family of separation logics for relaxed hardware memory models, and instantiate it on sequential consistency and on the Arm-A memory model. The Arm-A instance captures the fine-grained reasoning underpinning the low-overhead synchronisation idioms used by high-performance systems code. We mechanise AxSL in the Iris separation logic framework, illustrate it on key examples, and prove it sound with respect to the axiomatic memory model of Arm-A.<\/jats:p>\n                  <jats:p>By instantiating AxSL on different memory models, we demonstrate the generality of our approach, and show that it is largely generic in the axiomatic model and in the instruction-set semantics, offering a potential way forward for compositional reasoning for other models, and for the combination of production concurrency models and full-scale ISAs.<\/jats:p>","DOI":"10.1145\/3786762","type":"journal-article","created":{"date-parts":[[2026,1,19]],"date-time":"2026-01-19T11:13:32Z","timestamp":1768821212000},"page":"1-66","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["An Axiomatic Basis for Computer Programming on Relaxed Hardware Architectures: The AxSL Logics"],"prefix":"10.1145","volume":"48","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9652-4869","authenticated-orcid":false,"given":"Zongyuan","family":"Liu","sequence":"first","affiliation":[{"name":"Department of Computer Science, Aarhus University, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9156-9240","authenticated-orcid":false,"given":"Angus","family":"Hammond","sequence":"additional","affiliation":[{"name":"Computer Laboratory, University of Cambridge, Cambridge, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-0005-7618","authenticated-orcid":false,"given":"Thibaut","family":"P\u00e9rami","sequence":"additional","affiliation":[{"name":"Computer Laboratory, University of Cambridge, Cambridge, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9352-1013","authenticated-orcid":false,"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"Computer Laboratory, University of Cambridge, Cambridge, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Aarhus University, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4442-6543","authenticated-orcid":false,"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Aarhus University, Aarhus, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2026,3,19]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009883"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3458926"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","unstructured":"Jade Alglave Richard Grisenthwaite Artem Khyzha Luc Maranget and Nikos Nikoleris. 2024. Puss in boots: Formalizing arm\u2019s virtual memory system architecture. IEEE Micro 44 6 (2024) 83\u201391. DOI: 10.1109\/MM.2024.3422668","DOI":"10.1109\/MM.2024.3422668"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3177156"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","unstructured":"Jade Alglave Luc Maranget and Michael Tautschnig. 2014. Herding cats: Modelling simulation testing and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36 2 Article 7 (2014) 1\u201374. DOI: 10.1145\/2627752","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_8_1","unstructured":"Arm Ltd. 2023. ARM Architecture Reference Manual (for A-profile architecture). Arm Ltd. ARM DDI 0487J.a (ID042523) Retrieved April 7 2023 from https:\/\/developer.arm.com\/documentation\/ddi0487\/latest\/"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_14"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","unstructured":"Mark Batty Kayvan Memarian Kyndylan Nienhuis Jean Pichon-Pharabod and Peter Sewell. 2015. The problem of programming language concurrency semantics. In European Symposium on Programming (ESOP) 283\u2013307. DOI: 10.1007\/978-3-662-46669-8_12","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_13_1","unstructured":"P. Becker (Ed.) 2011. Programming Languages\u2014C++. ISO\/IEC 14882:2011. Retrieved from http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2011\/n3242.pdf"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_9"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_3_2_16_1","unstructured":"Richard Bornat Jade Alglave and Matthew J. Parkinson. 2015. New lace and arsenic: Adventures in weak memory with a program logic. arXiv:1512.01416. Retrieved from http:\/\/arxiv.org\/abs\/1512.01416"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","unstructured":"Stephen Brookes and Peter W. O\u2019Hearn. 2016. Concurrent separation logic. ACM SIGLOG News 3 3 (2016) 47\u201365. DOI: 10.1145\/2984450.2984457","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290383"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523718"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676984"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2020.11"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","unstructured":"Sadegh Dalvandi Brijesh Dongol Simon Doherty and Heike Wehrheim. 2022. Integrating Owicki-Gries for C11-style memory models into Isabelle\/HOL. J. Autom. Reason. 66 1 (2022) 141\u2013171. DOI: 10.1007\/S10817-021-09610-2","DOI":"10.1007\/S10817-021-09610-2"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_3_2_25_1","unstructured":"Will Deacon. 2016. The ARMv8 Application Level Memory Model. Retrieved from https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/aarch64.cat."},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293883.3295702"},{"key":"e_1_3_2_29_1","unstructured":"Marko Doko. 2021. Program Logic for Weak Memory Concurrency. Ph.\u2009D. dissertation. Kaiserslautern University of Technology Germany. Retrieved from https:\/\/kluedo.ub.rptu.de\/frontdoor\/index\/index\/docId\/6679"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_20"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_17"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009839"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_3_2_36_1","unstructured":"Kourosh Gharachorloo. 1995. Memory Consistency Models for Shared-Memory Multiprocessors. Ph.\u2009D. Dissertation. Stanford University."},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632863"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/PDP.2016.103"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1189736.1189737"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","unstructured":"C. A. R. Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12 10 (1969) 576\u2013580. DOI: 10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_42_1","unstructured":"Bart Jacobs. 2014. Verifying TSO Programs (Report CW660). Technical Report."},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934536"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429105"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018) e20. DOI: 10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPP.1993.15"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37706-8_11"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_25"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","unstructured":"Leslie Lamport. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3 2 (1977) 125\u2013143. DOI: 10.1109\/TSE.1977.229904","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591279"},{"key":"e_1_3_2_56_1","unstructured":"Yatin A. Manerkar Caroline Trippel Daniel Lustig Michael Pellauer and Margaret Martonosi. 2016. Counterexamples and proof loophole for the C\/C++ to POWER and ARMv7 trailing-sync compiler mappings. arXiv:1611.01507. Retrieved from http:\/\/arxiv.org\/abs\/1611.01507"},{"key":"e_1_3_2_57_1","unstructured":"Paul E. McKenney Ulrich Weigand Andrea Parri Boqun Feng and Alan Stern. 2020. Linux-Kernel Memory Model. ISO\/IEC JTC1 SC22 WG21 P0124R7. Retrieved from https:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2020\/p0124r7.html"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408978"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","unstructured":"F. L. Morris and C. B. Jones. 1984. An early program proof by Alan turing. Ann. History Comput. 6 2 (1984) 139\u2013143. DOI: 10.1109\/MAHC.1984.10017","DOI":"10.1109\/MAHC.1984.10017"},{"key":"e_1_3_2_60_1","unstructured":"Magnus O. Myreen. 2009. Formal Verification of Machine-Code Programs. Ph.\u2009D. Dissertation. University of Cambridge."},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75698-9_18"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_44"},{"key":"e_1_3_2_63_1","doi-asserted-by":"crossref","unstructured":"Magnus O. Myreen Michael J. C. Gordon and Konrad Slind. 2008. Machine-code verification for multiple architectures - An application of decompilation into logic. In Formal Methods in Computer-Aided Design (FMCAD). Alessandro Cimatti and Robert B. Jones (Eds.) IEEE 1\u20138.","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"e_1_3_2_64_1","doi-asserted-by":"crossref","unstructured":"Peter Naur. 1966. Proofs of algorithms by general snapshots. BIT 6 (1966) 310\u2013316.","DOI":"10.1007\/BF01966091"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","unstructured":"Susan S. Owicki and David Gries. 1976. An axiomatic proof technique for parallel programs I. Acta Informatica 6 (1976) 319\u2013340. DOI: 10.1007\/BF00268134","DOI":"10.1007\/BF00268134"},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"e_1_3_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_3_2_70_1","doi-asserted-by":"publisher","unstructured":"Christopher Pulte. 2018. The Semantics of Multicopy Atomic ARMv8 and RISC-V. Ph.\u2009D. Dissertation. University of Cambridge UK. DOI: 10.17863\/CAM.39379http:\/\/arxiv.org\/abs\/1611.01507","DOI":"10.17863\/CAM.39379http:\/\/arxiv.org\/abs\/1611.01507"},{"key":"e_1_3_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_3_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314624"},{"key":"e_1_3_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3776650"},{"key":"e_1_3_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428219"},{"key":"e_1_3_2_75_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15057-9_4"},{"key":"e_1_3_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523434"},{"key":"e_1_3_2_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_3_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_3_2_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_30"},{"key":"e_1_3_2_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/3695053.3731102"},{"key":"e_1_3_2_83_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_6"},{"key":"e_1_3_2_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_23"},{"key":"e_1_3_2_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_3_2_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57267-8_8"},{"key":"e_1_3_2_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_11"},{"key":"e_1_3_2_88_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_2_89_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_13"},{"key":"e_1_3_2_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483560"},{"key":"e_1_3_2_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632851"},{"key":"e_1_3_2_92_1","first-page":"67","volume-title":"Report of a Conference on High Speed Automatic Calculating Machines","author":"Turing Alan M.","year":"1949","unstructured":"Alan M. Turing. 1949. Checking a large routine. In Report of a Conference on High Speed Automatic Calculating Machines. Mathematical Laboratory, Cambridge, UK, 67\u201369. Retrieved from https:\/\/turingarchive.kings.cam.ac.uk\/publications-lectures-and-talks-amtb\/amt-b-8"},{"key":"e_1_3_2_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_3_2_94_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_3_2_95_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622820"},{"key":"e_1_3_2_96_1","unstructured":"Andrew Waterman and Krste Asanovi\u0107. 2019. The RISC-V Instruction Set Manual Volume I: Unprivileged ISA Document Version 20191213. Technical Report. Retrieved from https:\/\/github.com\/riscv\/riscv-isa-manual\/releases\/download\/Ratified-IMAFDQC\/riscv-spec-20191213.pdf"},{"key":"e_1_3_2_97_1","unstructured":"Ian Wehrman. 2012. Weak-Memory Local Reasoning (Dissertation Draft). Ph.D. Dissertation. University of Texas at Austin."},{"key":"e_1_3_2_98_1","unstructured":"Ian Wehrman and Josh Berdine. 2011. A proposal for weak-memory local reasoning. In Low-level Languages and Applications(LOLA)."},{"key":"e_1_3_2_99_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_12"},{"key":"e_1_3_2_100_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_13"},{"key":"e_1_3_2_101_1","doi-asserted-by":"publisher","unstructured":"Daniel Wright Sadegh Dalvandi Mark Batty and Brijesh Dongol. 2023. Mechanised operational reasoning for C11 programs with relaxed dependencies. Formal Aspects Comput. 35 2 Article 10 (2023) 1\u201327. DOI: 10.1145\/3580285","DOI":"10.1145\/3580285"},{"key":"e_1_3_2_102_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_2_103_1","unstructured":"Yang Zhang and Xinyu Feng. 2014. Program Logic for Local Reasoning in TSO. Technical Report."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3786762","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T06:36:02Z","timestamp":1773988562000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3786762"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,19]]},"references-count":102,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,3,31]]}},"alternative-id":["10.1145\/3786762"],"URL":"https:\/\/doi.org\/10.1145\/3786762","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,19]]},"assertion":[{"value":"2024-10-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-12-08","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-03-19","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}