{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:59:44Z","timestamp":1750309184570,"version":"3.41.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Science Foundation","award":["2145367"],"award-info":[{"award-number":["2145367"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>\n            The Lamport diagram is a pervasive and intuitive tool for informal reasoning about \u201chappens-before\u201d relationships in a concurrent system. However, traditional axiomatic formalizations of Lamport diagrams can be painful to work with in a mechanized setting like Agda. We propose an alternative, inductive formalization \u2014 the\n            <jats:italic>causal separation diagram<\/jats:italic>\n            (CSD) \u2014 that takes inspiration from string diagrams and concurrent separation logic, but enjoys a graphical syntax similar to Lamport diagrams. Critically, CSDs are based on the idea that causal relationships between events are witnessed by the\n            <jats:italic>paths<\/jats:italic>\n            that information follows between them. To that end, we model \u201chappens-before\u201d as a dependent type of paths between events.\n          <\/jats:p>\n          <jats:p>\n            The inductive formulation of CSDs enables their\n            <jats:italic>interpretation<\/jats:italic>\n            into a variety of semantic domains. We demonstrate the interpretability of CSDs with a case study on properties of\n            <jats:italic>logical clocks<\/jats:italic>\n            , widely-used mechanisms for reifying causal relationships as data. We carry out this study by implementing a series of interpreters for CSDs, culminating in a generic proof of Lamport\u2019s\n            <jats:italic>clock condition<\/jats:italic>\n            that is parametric in a choice of clock. We instantiate this proof on Lamport\u2019s scalar clock, on Mattern\u2019s vector clock, and on the matrix clocks of Raynal et al. and of Wuu and Bernstein, yielding verified implementations of each. The CSD formalism and our case study are mechanized in the Agda proof assistant.\n          <\/jats:p>","DOI":"10.1145\/3649830","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"529-554","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Inductive Diagrams for Causal Reasoning"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8548-3683","authenticated-orcid":false,"given":"Jonathan","family":"Castello","sequence":"first","affiliation":[{"name":"University of California, Santa Cruz, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5702-0860","authenticated-orcid":false,"given":"Patrick","family":"Redmond","sequence":"additional","affiliation":[{"name":"University of California, Santa Cruz, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1374-7715","authenticated-orcid":false,"given":"Lindsey","family":"Kuper","sequence":"additional","affiliation":[{"name":"University of California, Santa Cruz, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(92)90107-7"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)00055-7"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.2009.33"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337215"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Alur Rajeev","key":"e_1_2_1_6_1","unstructured":"Rajeev Alur, Gerard J. Holzmann, and Doron Peled. 1996. An analyzer for message sequence charts. In Tools and Algorithms for the Construction and Analysis of Systems, Tiziana Margaria and Bernhard Steffen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 35\u201348. isbn:978-3-540-49874-2"},{"volume-title":"Component Specification Using Event Classes","author":"Bickford Mark","key":"e_1_2_1_7_1","unstructured":"Mark Bickford. 2009. Component Specification Using Event Classes. In Component-Based Software Engineering, Grace A. Lewis, Iman Poernomo, and Christine Hofmeister (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 140\u2013155. isbn:978-3-642-02414-6"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/37499.37515"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/128738.128742"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/7351.7478"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2021.14"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571257"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.04.003"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/296806.296824"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/214451.214456"},{"volume-title":"Interacting Quantum Observables","author":"Coecke Bob","key":"e_1_2_1_17_1","unstructured":"Bob Coecke and Ross Duncan. 2008. Interacting Quantum Observables. In Automata, Languages and Programming, Luca Aceto, Ivan Damg\u00e5rd, Leslie Ann Goldberg, Magn\u00fas M. Halld\u00f3rsson, Anna Ing\u00f3lfsd\u00f3ttir, and Igor Walukiewicz (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 298\u2013310. isbn:978-3-540-70583-3"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571248"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/66926.66963"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 11th Australian Computer Science Conference, 10","author":"Fidge C. J.","year":"1988","unstructured":"C. J. Fidge. 1988. Timestamps in message-passing systems that preserve the partial ordering. Proceedings of the 11th Australian Computer Science Conference, 10, 1 (1988), 56\u201366."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542490"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35394-4_1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434323"},{"key":"e_1_2_1_24_1","unstructured":"ITU-T. 2011. ITU Recommendation Z.120: Message Sequence Chart (MSC). https:\/\/www.itu.int\/rec\/T-REC-Z.120-201102-I\/"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(91)90003-p"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-003-0105-9"},{"volume-title":"Proceedings of the IFIP TC6\/WG6.1 Sixth International Conference on Formal Description Techniques, VI (FORTE \u201993)","author":"Peter","key":"e_1_2_1_29_1","unstructured":"Peter B. Ladkin and Stefan Leue. 1993. What Do Message Sequence Charts Mean? In Proceedings of the IFIP TC6\/WG6.1 Sixth International Conference on Formal Description Techniques, VI (FORTE \u201993). North-Holland Publishing Co., Nld. 301\u2013316. isbn:0444817735"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of IFIP Congress 1977 (IFIP \u201977)","author":"Lann G\u00e9rard Le","year":"1977","unstructured":"G\u00e9rard Le Lann. 1977. Distributed Systems \u2013 Toward a Formal Approach. In Proceedings of IFIP Congress 1977 (IFIP \u201977). North-Holland Publishing Co., Nld. 155\u2013160. isbn:0720407559"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","unstructured":"Adrian Lehmann Ben Caldwell and Robert Rand. 2022. VyZX: A Vision for Verifying the ZX Calculus. https:\/\/doi.org\/10.48550\/ARXIV.2205.05781 arxiv:2205.05781.","DOI":"10.48550\/ARXIV.2205.05781"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","unstructured":"Adrian Lehmann Ben Caldwell Bhakti Shah and Robert Rand. 2023. VyZX: Formal Verification of a Graphical Quantum Language. https:\/\/doi.org\/10.48550\/arXiv.2311.11571 arxiv:2311.11571.","DOI":"10.48550\/arXiv.2311.11571"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043593"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.10.002"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018611"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507734"},{"key":"e_1_2_1_39_1","unstructured":"Friedemann Mattern. 1989. Virtual Time and Global States of Distributed Systems. In Parallel and Distributed Algorithms. North-Holland 215\u2013226."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622876"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78142-2_13"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563351"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211968"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_46_1","unstructured":"Robin Piedeleu and Fabio Zanasi. 2023. An Introduction to String Diagrams for Computer Scientists. arxiv:2305.08768. arxiv:2305.08768"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/781498.781529"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.05.009"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90008-6"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.485846"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3587216.3587222"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_53_1","volume-title":"Heinrich Hu\u00df mann, and Manfred Broy","author":"Sch\u00e4tz Bernhard","year":"1996","unstructured":"Bernhard Sch\u00e4tz, Heinrich Hu\u00df mann, and Manfred Broy. 1996. Graphical development of consistent system specifications. In FME\u201996: Industrial Benefit and Advances in Formal Methods, Marie-Claude Gaudel and James Woodcock (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 248\u2013267. isbn:978-3-540-49749-3"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51687-5_45"},{"key":"e_1_2_1_55_1","unstructured":"Frank B Schmuck. 1988. The use of efficient broadcast protocols in asynchronous distributed systems. Ph. D. Dissertation."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/2050613.2050642"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/fmcad.2008.ecp.14"},{"key":"e_1_2_1_58_1","volume-title":"Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI \u201906)","author":"Weil Sage A.","year":"2006","unstructured":"Sage A. Weil, Scott A. Brandt, Ethan L. Miller, Darrell D. E. Long, and Carlos Maltzahn. 2006. Ceph: A Scalable, High-Performance Distributed File System. In Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI \u201906). USENIX Association, USA. 307\u2013320. isbn:1931971471"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_12"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/800222.806750"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649830","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649830","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:06Z","timestamp":1750287246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649830"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":60,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649830"],"URL":"https:\/\/doi.org\/10.1145\/3649830","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}