{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T14:59:46Z","timestamp":1780930786555,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T00:00:00Z","timestamp":1661904000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,8,31]]},"DOI":"10.1145\/3587216.3587222","type":"proceedings-article","created":{"date-parts":[[2023,6,5]],"date-time":"2023-06-05T22:16:00Z","timestamp":1686003360000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Verified Causal Broadcast with Liquid Haskell"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5702-0860","authenticated-orcid":false,"given":"Patrick","family":"Redmond","sequence":"first","affiliation":[{"name":"University of California, Santa Cruz, United States"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-0947-9531","authenticated-orcid":false,"given":"Gan","family":"Shen","sequence":"additional","affiliation":[{"name":"University of California, Santa Cruz, United States"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0732-5476","authenticated-orcid":false,"given":"Niki","family":"Vazou","sequence":"additional","affiliation":[{"name":"IMDEA Software, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1374-7715","authenticated-orcid":false,"given":"Lindsey","family":"Kuper","sequence":"additional","affiliation":[{"name":"University of California, Santa Cruz, United States"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,6,5]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(92)90107-7"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)00055-7"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/37499.37515"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/128738.128742"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/7351.7478"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009888"},{"key":"e_1_3_2_1_9_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, C.\u00a0R","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An Efficient SMT Solver . In Tools and Algorithms for the Construction and Analysis of Systems, C.\u00a0R . Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 337\u2013340. Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C.\u00a0R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337\u2013340."},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the 11th Australian Computer Science Conference 10","author":"Fidge J.","year":"1988","unstructured":"C.\u00a0 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. C.\u00a0J. 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_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133933"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434323"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_3_2_1_17_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . 2002 . Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley Longman Publishing Co., Inc. , USA. Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., USA."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428284"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043593"},{"key":"e_1_3_2_1_22_1","volume-title":"Technical Report TR-11-22. Computer Science Department","author":"Mahajan P.","year":"2011","unstructured":"P. Mahajan , L. Alvisi , and M. Dahlin . 2011 . Consistency , Availability, Convergence . Technical Report TR-11-22. Computer Science Department , University of Texas at Austin. P. Mahajan, L. Alvisi, and M. Dahlin. 2011. Consistency, Availability, Convergence. Technical Report TR-11-22. Computer Science Department, University of Texas at Austin."},{"key":"e_1_3_2_1_23_1","unstructured":"Friedemann Mattern. 1989. Virtual Time and Global States of Distributed Systems. In Parallel and Distributed Algorithms. North-Holland 215\u2013226.  Friedemann Mattern. 1989. Virtual Time and Global States of Distributed Systems. In Parallel and Distributed Algorithms. North-Holland 215\u2013226."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2808098.2808099"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563351"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"e_1_3_2_1_27_1","unstructured":"Jon Postel. 1981. Transmission Control Protocol. STD\u00a07. RFC Editor. http:\/\/www.rfc-editor.org\/rfc\/rfc793.txt  Jon Postel. 1981. Transmission Control Protocol. STD\u00a07. RFC Editor. http:\/\/www.rfc-editor.org\/rfc\/rfc793.txt"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90008-6"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51687-5_45"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2014.45"},{"key":"e_1_3_2_1_32_1","unstructured":"Frank\u00a0B Schmuck. 1988. The use of efficient broadcast protocols in asynchronous distributed systems. Ph.\u00a0D. Dissertation.  Frank\u00a0B Schmuck. 1988. The use of efficient broadcast protocols in asynchronous distributed systems. Ph.\u00a0D. Dissertation."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/2050613.2050642"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/155848.155857"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242756"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_3_2_1_40_1","volume-title":"Theorem Proving in Higher Order Logics, Otmane\u00a0Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.)","author":"Wenzel Makarius","unstructured":"Makarius Wenzel , Lawrence\u00a0 C. Paulson , and Tobias Nipkow . 2008. The Isabelle Framework . In Theorem Proving in Higher Order Logics, Otmane\u00a0Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.) . Springer Berlin Heidelberg , Berlin, Heidelberg , 33\u201338. Makarius Wenzel, Lawrence\u00a0C. Paulson, and Tobias Nipkow. 2008. The Isabelle Framework. In Theorem Proving in Higher Order Logics, Otmane\u00a0Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 33\u201338."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"}],"event":{"name":"IFL 2022: Symposium on Implementation and Application of Functional Languages","location":"Copenhagen Denmark","acronym":"IFL 2022"},"container-title":["Proceedings of the 34th Symposium on Implementation and Application of Functional Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3587216.3587222","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3587216.3587222","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:15Z","timestamp":1750178835000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3587216.3587222"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,31]]},"references-count":41,"alternative-id":["10.1145\/3587216.3587222","10.1145\/3587216"],"URL":"https:\/\/doi.org\/10.1145\/3587216.3587222","relation":{},"subject":[],"published":{"date-parts":[[2022,8,31]]},"assertion":[{"value":"2023-06-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}