{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T15:57:56Z","timestamp":1787068676270,"version":"3.56.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>\n                    The release of OCaml 5, which introduced parallelism in the OCaml runtime, drove the need for safe and efficient concurrent data structures. New libraries like\n                    <jats:monospace>Saturn<\/jats:monospace>\n                    address this need. This is an opportunity to apply and further state-of-the-art program verification techniques.\n                  <\/jats:p>\n                  <jats:p>\n                    We present Zoo, a framework for verifying fine-grained concurrent OCaml 5 algorithms. Following a pragmatic approach, we defined a limited but sufficient fragment of the language to faithfully express these algorithms: ZooLang. We formalized its semantics carefully via a deep embedding in the Rocq proof assistant, uncovering subtle aspects of physical equality. We provide a tool to translate source OCaml programs into ZooLang syntax embedded inside Rocq, where they can be specified and verified using the Iris concurrent separation logic. To illustrate the applicability of Zoo, we verified a subset of the standard library and a collection of fined-grained concurrent data structures from the\n                    <jats:monospace>Saturn<\/jats:monospace>\n                    and\n                    <jats:monospace>Eio<\/jats:monospace>\n                    libraries.\n                  <\/jats:p>\n                  <jats:p>In the process, we also extended OCaml to more efficiently express certain concurrent programs.<\/jats:p>","DOI":"10.1145\/3776701","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1702-1729","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-2972-5181","authenticated-orcid":false,"given":"Cl\u00e9ment","family":"Allain","sequence":"first","affiliation":[{"name":"INRIA, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1758-3938","authenticated-orcid":false,"given":"Gabriel","family":"Scherer","sequence":"additional","affiliation":[{"name":"INRIA, Paris, France"},{"name":"Universit\u00e9 Paris Cit\u00e9, IRIF, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674637"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_5"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473586"},{"key":"e_1_3_2_5_1","volume-title":"Accreditation to supervise research","author":"Boulm\u00e9 Sylvain","year":"2021","unstructured":"Sylvain Boulm\u00e9. 2021. Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles). Accreditation to supervise research. Universit\u00e9 Grenoble-Alpes. https:\/\/hal.science\/tel-03356701 see also http:\/\/www-verimag.imag.fr\/boulme\/hdr.html."},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-014-9306-0"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_8_1","first-page":"871","volume-title":"In 17th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2023, Boston, MA, USA, July 10-12, 2023","author":"Chang Yun-Sheng","year":"2023","unstructured":"Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. 2023. Verifying vMVCC, a high-performance transaction library using multi-version concurrency control. In 17th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2023, Boston, MA, USA, July 10-12, 2023, Roxana Geambasu and Ed Nightingale (Eds.). USENIX Association, 871\u2013886. https:\/\/www.usenix.org\/conference\/osdi23\/presentation\/chang"},{"key":"e_1_3_2_9_1","volume-title":"(Un nouveau regard sur la Logique de S\u00e9paration pour les programmes s\u00e9quentiels)","author":"Chargu\u00e9raud Arthur","year":"2023","unstructured":"Arthur Chargu\u00e9raud. 2023. Habilitation thesis: A Modern Eye on Separation Logic for Sequential Programs. (Un nouveau regard sur la Logique de S\u00e9paration pour les programmes s\u00e9quentiels). Universit\u00e9 de Strasbourg. https:\/\/tel.archives-ouvertes.fr\/tel-04076725"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_29"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1073970.1073974"},{"key":"e_1_3_2_12_1","volume-title":"coq-of-ocaml","author":"Claret Guillaume","year":"2025","unstructured":"Guillaume Claret. 2025. coq-of-ocaml. https:\/\/github.com\/formal-land\/coq-of-ocaml"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292535.1292541"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","unstructured":"Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2021. A separation logic for effect handlers. Proc. ACM Program. Lang. 5 POPL (2021) 1\u201328. doi:10.1145\/3434314","DOI":"10.1145\/3434314"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192421"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","unstructured":"Lennard G\u00e4her Michael Sammler Ralf Jung Robbert Krebbers and Derek Dreyer. 2024. RefinedRust: A Type System for High-Assurance Verification of Rust Programs. Proc. ACM Program. Lang. 8 PLDI (2024) 1115\u20131139. doi:10.1145\/3656422","DOI":"10.1145\/3656422"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","unstructured":"A\u00efna Linn Georges Benjamin Peters Laila Elbeheiry Leo White Stephen Dolan Richard A. Eisenberg Chris Casinghino Fran\u00e7ois Pottier and Derek Dreyer. 2025. Data Race Freedom \u00e0 la Mode. Proc. ACM Program. Lang. 9 POPL (2025) 656\u2013686. doi:10.1145\/3704859","DOI":"10.1145\/3704859"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","unstructured":"L\u00e9on Gondelman Jonas Kastberg Hinrichsen M\u00e1rio Pereira Amin Timany and Lars Birkedal. 2023. Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols. Proc. ACM Program. Lang. 7 ICFP (2023) 847\u2013877. doi:10.1145\/3607859","DOI":"10.1145\/3607859"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636961"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","unstructured":"Maurice Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst. 12 3 (1990) 463\u2013492. doi:10.1145\/78969.78972","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_24_1","unstructured":"Iris development team. 2025. Iris examples. https:\/\/gitlab.mpi-sws.org\/iris\/examples\/"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_2_26_1","volume-title":"(Verasco: un analyseur statique pour C formellement v\u00e9rifi\u00e9). Ph. D. Dissertation. l:Paris Diderot University","author":"Jourdan Jacques-Henri","year":"2016","unstructured":"Jacques-Henri Jourdan. 2016. Verasco: a Formally Verified C Static Analyzer. (Verasco: un analyseur statique pour C formellement v\u00e9rifi\u00e9). Ph. D. Dissertation. l:Paris Diderot University, France. https:\/\/tel.archives-ouvertes.fr\/tel-01327023"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Rodolphe Lepigre Gaurav Parthasarathy Marianna Rapoport Amin Timany Derek Dreyer and Bart Jacobs. 2020. The future is ours: prophecy variables in separation logic. Proc. ACM Program. Lang. 4 POPL (2020) 45:1\u201345:32. doi:10.1145\/3371113","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_30_1","unstructured":"Vesa Karvonen. 2025a. Kcas. https:\/\/github.com\/ocaml-multicore\/kcas"},{"key":"e_1_3_2_31_1","unstructured":"Vesa Karvonen. 2025b. Picos. https:\/\/github.com\/ocaml-multicore\/picos"},{"key":"e_1_3_2_32_1","unstructured":"Vesa Karvonen and Carine Morel. 2025. Saturn. https:\/\/github.com\/ocaml-multicore\/saturn"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. MoSeL: a general extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang. 2 ICFP (2018) 77:1\u201377:30. doi:10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_35_1","unstructured":"Anil Madhavapeddy and Thomas Leonard. 2025. Eio. https:\/\/github.com\/ocaml-multicore\/eio"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","unstructured":"Glen M\u00e9vel and Jacques-Henri Jourdan. 2021. Formal verification of a concurrent bounded queue in a weak memory model. Proc. ACM Program. Lang. 5 ICFP (2021) 1\u201329. doi:10.1145\/3473571","DOI":"10.1145\/3473571"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","unstructured":"Glen M\u00e9vel Jacques-Henri Jourdan and Fran\u00e7ois Pottier. 2020. Cosmo: a concurrent separation logic for multicore OCaml. Proc. ACM Program. Lang. 4 ICFP (2020) 96:1\u201396:29. doi:10.1145\/3408978","DOI":"10.1145\/3408978"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","unstructured":"Ike Mulder and Robbert Krebbers. 2023. Proof Automation for Linearizability in Separation Logic. Proc. ACM Program. Lang. 7 OOPSLA1 (2023) 462\u2013491. doi:10.1145\/3586043","DOI":"10.1145\/3586043"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-810-5-104"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_31"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","unstructured":"Christopher Pulte Dhruv C. Makwana Thomas Sewell Kayvan Memarian Peter Sewell and Neel Krishnaswami. 2023. CN: Verifying Systems C Code with Separation-Logic Refinement Types. Proc. ACM Program. Lang. 7 POPL (2023) 1\u201332. doi:10.1145\/3571194","DOI":"10.1145\/3571194"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","unstructured":"Remy Seassau Irene Yoon Jean-Marie Madiot and Fran\u00e7ois Pottier. 2025. Formal Semantics and Program Logics for a Fragment of OCaml. Proc. ACM Program. Lang. 9 ICFP Article 240 (Aug. 2025) 32 pages. doi:10.1145\/3747509","DOI":"10.1145\/3747509"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","unstructured":"Daniel Selsam Simon Hudon and Leonardo de Moura. 2020. Sealing pointer-based optimizations behind pure functions. Proc. ACM Program. Lang. 4 ICFP (2020) 115:1\u2013115:20. doi:10.1145\/3408997","DOI":"10.1145\/3408997"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408995"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454039"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167092"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000142"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439931"},{"key":"e_1_3_2_52_1","volume-title":"International Business Machines Incorporated","author":"Treiber R. K.","year":"1986","unstructured":"R. K. Treiber. 1986. Systems Programming: Coping with Parallelism. International Business Machines Incorporated, Thomas J. Watson Research Center. https:\/\/books.google.fr\/books?id=YQg3HAAACAAJ"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439930"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503689"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776701","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:45:28Z","timestamp":1784209528000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776701"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":53,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776701"],"URL":"https:\/\/doi.org\/10.1145\/3776701","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}