{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T01:27:37Z","timestamp":1778635657334,"version":"3.51.4"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","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,10,8]]},"abstract":"<jats:p>\n                    We introduce Multris, a separation logic for verifying functional correctness of programs that combine multiparty message-passing communication with shared-memory concurrency. The foundation of our work is a novel concept of multiparty\n                    <jats:italic toggle=\"yes\">protocol consistency<\/jats:italic>\n                    , which guarantees safe communication among a set of parties, provided each party adheres to its prescribed protocol. Our concept of protocol consistency is inspired by the bottom-up approach for multiparty session types. However, by considering it in the context of separation logic instead of a type system, we go further in terms of generality by supporting new notions of\n                    <jats:italic toggle=\"yes\">implicit transfer of knowledge<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">implicit transfer of resources<\/jats:italic>\n                    . We develop tactics for automatically verifying protocol consistency and for reasoning about message-passing operations in Multris. We evaluate Multris on a range of examples, including the well-known two- and three-buyer protocols, as well as a new verification benchmark based on Chang and Roberts's ring leader election protocol. To ensure the reliability of our work, we prove soundness of Multris w.r.t. a low-level channel semantics using the Iris framework in Coq.\n                  <\/jats:p>","DOI":"10.1145\/3689762","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"1446-1474","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Multris: Functional Verification of Multiparty Message Passing in Separation Logic"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6143-9031","authenticated-orcid":false,"given":"Jonas Kastberg","family":"Hinrichsen","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus N, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1976-3182","authenticated-orcid":false,"given":"Jules","family":"Jacobs","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/1037736"},{"key":"e_1_3_1_3_2","article-title":"Solving Reflexive Domain Equations in a Category of Complete Metric Spaces","author":"America Pierre","year":"1989","unstructured":"Pierre America and Jan J. M. M. Rutten. 1989. Solving Reflexive Domain Equations in a Category of Complete Metric Spaces. JCSS (1989). https:\/\/doi.org\/10.1016\/0022-0000(89)90027-5 10.1016\/0022-0000(89)90027-5","journal-title":"JCSS"},{"key":"e_1_3_1_4_2","article-title":"Foundational Proof-Carrying Code","author":"Appel Andrew W.","year":"2001","unstructured":"Andrew W. Appel . 2001. Foundational Proof-Carrying Code. In LICS. https:\/\/doi.org\/10.1109\/LICS.2001.932501 10.1109\/LICS.2001.932501","journal-title":"LICS"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_1_6_2","article-title":"A very modal model of a modern, major, general type system","author":"Appel Andrew W.","year":"2007","unstructured":"Andrew W. Appel, Paul-Andr\u00e9 Melli\u00e8s, Christopher D. Richards, and J\u00e9r\u00f4me Vouillon. 2007. A very modal model of a modern, major, general type system. In POPL. https:\/\/doi.org\/10.1145\/1190216.1190235 10.1145\/1190216.1190235","journal-title":"POPL"},{"key":"e_1_3_1_7_2","article-title":"Global Progress in Dynamically Interleaved Multiparty Sessions","author":"Bettini Lorenzo","year":"2008","unstructured":"Lorenzo Bettini, Mario Coppo, Loris D'Antoni, Marco De Luca, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. 2008. Global Progress in Dynamically Interleaved Multiparty Sessions. In CONCUR. https:\/\/doi.org\/10.1007\/978-3-540-85361-9_33 10.1007\/978-3-540-85361-9_33","journal-title":"CONCUR"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.07.010"},{"key":"e_1_3_1_9_2","article-title":"A Theory ofDesign-by-Contract for Distributed Multiparty Interactions","author":"LauraBocchi Kohei Honda","year":"2010","unstructured":"LauraBocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. 2010. A Theory ofDesign-by-Contract for Distributed Multiparty Interactions. In CONCUR. https:\/\/doi.org\/10.1007\/978-3-642-15375-4_12 10.1007\/978-3-642-15375-4_12","journal-title":"CONCUR"},{"key":"e_1_3_1_10_2","article-title":"Zooid:ADSL for Certified Multiparty Computation: From Mechanised Metatheory to Certified Multiparty Processes","author":"Castro-Perez David","year":"2021","unstructured":"David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, and Nobuko Yoshida. 2021. Zooid:ADSL for Certified Multiparty Computation: From Mechanised Metatheory to Certified Multiparty Processes. In PLDI.https:\/\/doi.org\/10.1145\/3453483.3454041 10.1145\/3453483.3454041","journal-title":"PLDI"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359108"},{"key":"e_1_3_1_12_2","article-title":"Towards a Session Logic for Communication Protocols","author":"Craciun Florin","year":"2015","unstructured":"Florin Craciun, Tibor Kiss, and Andreea Costea. 2015. Towards a Session Logic for Communication Protocols. In ICECCS. https:\/\/doi.org\/10.1109\/ICECCS.2015.33 10.1109\/ICECCS.2015.33","journal-title":"ICECCS"},{"key":"e_1_3_1_13_2","article-title":"Concurrent Abstract Predicates","author":"Dinsdale-Young Thomas","year":"2010","unstructured":"Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP.https:\/\/doi.org\/10.1007\/978-3-642-14107-2_24 10.1007\/978-3-642-14107-2_24","journal-title":"ECOOP"},{"key":"e_1_3_1_14_2","article-title":"Permission-Based Separation Logic for MessagePassing Concurrency","author":"Francalanza Adrian","year":"2011","unstructured":"Adrian Francalanza, Julian Rathke, and Vladimiro Sassone. 2011. Permission-Based Separation Logic for MessagePassing Concurrency. LMCS (2011). https:\/\/doi.org\/10.2168\/LMCS-7(3:7)2011 10.2168\/LMCS-7(3:7)2011","journal-title":"LMCS"},{"key":"e_1_3_1_15_2","article-title":"Linear type theory for asynchronous session types","author":"Gay Simon J.","year":"2010","unstructured":"Simon J. Gay and Vasco Thudichum Vasconcelos. 2010. Linear type theory for asynchronous session types. JFP (2010). https:\/\/doi.org\/10.1017\/S0956796809990268 10.1017\/S0956796809990268","journal-title":"JFP"},{"key":"e_1_3_1_16_2","article-title":"Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols","author":"Gondelman Leon","year":"2023","unstructured":"Leon Gondelman, Jonas Kastberg Hinrichsen, Mario Pereira, Amin Timany, and Lars Birkedal. 2023. Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols. ICFP (2023). https:\/\/doi.org\/10.1145\/3607859 10.1145\/3607859","journal-title":"ICFP"},{"key":"e_1_3_1_17_2","article-title":"Actris: Session-Type Based Reasoning in Separation Logic","author":"Hinrichsen Jonas Kastberg","year":"2020","unstructured":"Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers. 2020. Actris: Session-Type Based Reasoning in Separation Logic. POPL (2020). https:\/\/doi.org\/10.1145\/3371074 10.1145\/3371074","journal-title":"POPL"},{"key":"e_1_3_1_18_2","article-title":"Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic","author":"Hinrichsen Jonas Kastberg","year":"2022","unstructured":"Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers. 2022. Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic. LMCS (2022). https:\/\/doi.org\/10.46298\/lmcs-18(2:16)2022 10.46298\/lmcs-18(2:16)2022","journal-title":"LMCS"},{"key":"e_1_3_1_19_2","unstructured":"Jonas Kastberg Hinrichsen Jules Jacobs and Robbert Krebbers. 2024. Coq Mechanization of \u201cMultris: Functional Verification of Multiparty Message Passing in Separation Logic\u201d. https:\/\/doi.org\/10.5281\/zenodo.13380561 10.5281\/zenodo.13380561"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439914"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_3_1_22_2","article-title":"Language Primitives and Type Discipline for Structured Communication-Based Programming","author":"Honda Kohei","year":"1998","unstructured":"Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In ESOP. https:\/\/doi.org\/10.1007\/BFb0053567 10.1007\/BFb0053567","journal-title":"ESOP"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_3_1_25_2","article-title":"Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom","author":"Jacobs Jules","year":"2022","unstructured":"Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom. ICFP (2022). https:\/\/doi.org\/10.1145\/3547638 10.1145\/3547638","journal-title":"ICFP"},{"key":"e_1_3_1_26_2","article-title":"Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)","author":"Jacobs Jules","year":"2023","unstructured":"Jules Jacobs, Jonas Kastberg Hinrichsen, and Robbert Krebbers. 2023. Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl). ICFP (2023). https:\/\/doi.org\/10.1145\/3607856 10.1145\/3607856","journal-title":"ICFP"},{"key":"e_1_3_1_27_2","article-title":"Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing","author":"Jacobs Jules","year":"2024","unstructured":"Jules Jacobs, Jonas Kastberg Hinrichsen, and Robbert Krebbers. 2024. Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. POPL (2024). https:\/\/doi.org\/10.1145\/3632889 10.1145\/3632889","journal-title":"POPL"},{"key":"e_1_3_1_28_2","article-title":"Higher-order ghost state","author":"Jung Ralf","year":"2016","unstructured":"Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. https:\/\/doi.org\/10.1145\/2951913.2951943 10.1145\/2951913.2951943","journal-title":"ICFP"},{"key":"e_1_3_1_29_2","article-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic","author":"Jung Ralf","year":"2018","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. JFP (2018). https:\/\/doi.org\/10.1017\/S0956796818000151 10.1017\/S0956796818000151","journal-title":"JFP"},{"key":"e_1_3_1_30_2","article-title":"Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning","author":"Jung Ralf","year":"2015","unstructured":"Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. https:\/\/doi.org\/10.1145\/2676726.2676980 10.1145\/2676726.2676980","journal-title":"POPL"},{"key":"e_1_3_1_31_2","doi-asserted-by":"crossref","unstructured":"Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargueraud and Derek Dreyer. 2018. MoSeL: A General Extensible Modal Framework for Interactive Proofs in Separation Logic. ICFP (2018). https:\/\/doi.org\/10.1145\/3236772 10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"e_1_3_1_32_2","article-title":"The Essence of Higher-Order Concurrent Separation Logic","author":"Krebbers Robbert","year":"2017","unstructured":"Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In ESOP. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26 10.1007\/978-3-662-54434-1_26","journal-title":"ESOP"},{"key":"e_1_3_1_33_2","article-title":"Interactive Proofs in Higher-Order Concurrent Separation Logic","author":"Krebbers Robbert","year":"2017","unstructured":"Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive Proofs in Higher-Order Concurrent Separation Logic. In POPL. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","journal-title":"POPL"},{"key":"e_1_3_1_34_2","article-title":"Complete Multiparty Session Type Projection with Automata","author":"Li Elaine","year":"2023","unstructured":"Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. 2023. Complete Multiparty Session Type Projection with Automata. In CAV 2023. https:\/\/doi.org\/10.1007\/978-3-031-37709-9_17 10.1007\/978-3-031-37709-9_17","journal-title":"CAV"},{"key":"e_1_3_1_35_2","article-title":"Shared Contract-ObedientEndpoints","author":"Lozes Etienne","year":"2012","unstructured":"Etienne Lozes and Jules Villard. 2012. Shared Contract-ObedientEndpoints. In ICE. https:\/\/doi.org\/10.4204\/EPTCS.104.3 10.4204\/EPTCS.104.3","journal-title":"ICE."},{"key":"e_1_3_1_36_2","article-title":"Global Principal Typing in Partially Commutative Asynchronous Sessions","author":"Mostrous Dimitris","year":"2009","unstructured":"Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. 2009. Global Principal Typing in Partially Commutative Asynchronous Sessions. In ESOP. https:\/\/doi.org\/10.1007\/978-3-642-00590-9_23 10.1007\/978-3-642-00590-9_23","journal-title":"ESOP"},{"key":"e_1_3_1_37_2","article-title":"A modality for recursion","author":"Nakano Hiroshi","year":"2000","unstructured":"Hiroshi Nakano . 2000. A modality for recursion. In LICS. https:\/\/doi.org\/10.1109\/LICS.2000.855774 10.1109\/LICS.2000.855774","journal-title":"LICS"},{"key":"e_1_3_1_38_2","article-title":"Future-based Static Analysis of Message Passing Programs","author":"Oortwijn Wytse","year":"2016","unstructured":"Wytse Oortwijn, Stefan Blom, and Marieke Huisman. 2016. Future-based Static Analysis of Message Passing Programs. In PLACES. https:\/\/doi.org\/10.4204\/EPTCS.211.7 10.4204\/EPTCS.211.7","journal-title":"PLACES"},{"key":"e_1_3_1_39_2","article-title":"Less is more: multiparty session types revisited","author":"Scalas Alceste","year":"2019","unstructured":"Alceste Scalas and Nobuko Yoshida. 2019. Less is more: multiparty session types revisited. POPL (2019). https:\/\/doi.org\/10.1145\/3290343 10.1145\/3290343","journal-title":"POPL"},{"key":"e_1_3_1_40_2","article-title":"Verified Lock-Free Session Channels with Linking","author":"Somers Thomas","year":"2024","unstructured":"Thomas Somers and Robbert Krebbers. 2024. Verified Lock-Free Session Channels with Linking. OOPSLA (2024). https:\/\/doi.org\/10.1145\/3689732 10.1145\/3689732","journal-title":"OOPSLA"},{"key":"e_1_3_1_41_2","article-title":"Impredicative Concurrent Abstract Predicates","author":"Svendsen Kasper","year":"2014","unstructured":"Kasper Svendsen and Lars Birkedal. 2014. Impredicative Concurrent Abstract Predicates. In ESOP. https:\/\/doi.org\/10.1007\/978-3-642-54833-8_9 10.1007\/978-3-642-54833-8_9","journal-title":"ESOP"},{"key":"e_1_3_1_42_2","article-title":"Dependent types and multi-monadic effects in F*","author":"Swamy Nikhil","year":"2016","unstructured":"Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, C\u00e9dric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella B\u00e9guelin. 2016. Dependent types and multi-monadic effects in F*. In POPL. https:\/\/doi.org\/10.1145\/2837614.2837655 10.1145\/2837614.2837655","journal-title":"POPL"},{"key":"e_1_3_1_43_2","article-title":"Why Do Scala Developers Mix the Actor Model with other Concurrency Models?","author":"Tasharofi Samira","year":"2013","unstructured":"Samira Tasharofi, Peter Dinges, and Ralph E. Johnson. 2013. Why Do Scala Developers Mix the Actor Model with other Concurrency Models?. In ECOOP. https:\/\/doi.org\/10.1007\/978-3-642-39038-8_13 10.1007\/978-3-642-39038-8_13","journal-title":"ECOOP"},{"key":"e_1_3_1_44_2","doi-asserted-by":"crossref","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2024. A Logical Approach to Type Soundness. To appear in JACM.","DOI":"10.1145\/3676954"},{"key":"e_1_3_1_45_2","article-title":"A Sound and Complete Projection for Global Types","author":"Tirore Dawit Legesse","year":"2023","unstructured":"Dawit Legesse Tirore, Jesper Bengtson, and Marco Carbone. 2023. A Sound and Complete Projection for Global Types. In ITP (LIPIcs). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2023.28 10.4230\/LIPICS.ITP.2023.28","journal-title":"ITP (LIPIcs)"},{"key":"e_1_3_1_46_2","first-page":"865","article-title":"Understanding Real-World Concurrency Bugs in Go","author":"Tengfei Tu","year":"2019","unstructured":"Tengfei Tu, Xiaoyu Liu, Linhai Song, and Yiying Zhang. 2019. Understanding Real-World Concurrency Bugs in Go. In ASPLOS. 865-878. https:\/\/doi.org\/10.1145\/3297858.3304069 10.1145\/3297858.3304069","journal-title":"ASPLOS."},{"key":"e_1_3_1_47_2","article-title":"Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency","author":"Turon Aaron","year":"2013","unstructured":"Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In ICFP. https:\/\/doi.org\/10.1145\/2500365.2500600 10.1145\/2500365.2500600","journal-title":"ICFP"},{"key":"e_1_3_1_48_2","article-title":"Statically verified refinements for multiparty protocols","author":"Zhou Fangyi","year":"2020","unstructured":"Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. 2020. Statically verified refinements for multiparty protocols. OOPSLA (2020). https:\/\/doi.org\/10.1145\/3428216 10.1145\/3428216","journal-title":"OOPSLA"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689762","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689762","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:04:14Z","timestamp":1770195854000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689762"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":47,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689762"],"URL":"https:\/\/doi.org\/10.1145\/3689762","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}