{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T21:15:51Z","timestamp":1775769351470,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","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"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101096090"],"award-info":[{"award-number":["101096090"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,1,8]]},"DOI":"10.1145\/3779031.3779109","type":"proceedings-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:55:47Z","timestamp":1767898547000},"page":"368-382","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-9568-4592","authenticated-orcid":false,"given":"Virgil","family":"Marionneau","sequence":"first","affiliation":[{"name":"ENS Rennes, Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-7559-1326","authenticated-orcid":false,"given":"F\u00e9lix","family":"Sassus Bourda","sequence":"additional","affiliation":[{"name":"ENS Paris-Saclay, Gif-sur-Yvette, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6746-2734","authenticated-orcid":false,"given":"Alejandro","family":"Aguirre","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674635"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(1:3)2015"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704876"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704894"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_5"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2016.107"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480894"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103670"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.7561\/SACS.2014.2.177"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802212"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632868"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704877"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591226"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704899"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17800602"},{"key":"e_1_3_2_1_22_1","volume-title":"Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814075"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622870"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2018.141"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","unstructured":"The Rocq Development Team. 2025. The Rocq Prover. https:\/\/doi.org\/10.5281\/zenodo.15149629 10.5281\/zenodo.15149629","DOI":"10.5281\/zenodo.15149629"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Noam Zilberstein Alexandra Silva and Joseph Tassarotti. 2025. Probabilistic Concurrent Reasoning in Outcome Logic: Independence Conditioning and Invariants. https:\/\/doi.org\/10.48550\/arXiv.2411.11662 arXiv:2411.11662 [cs] 10.48550\/arXiv.2411.11662","DOI":"10.48550\/arXiv.2411.11662"}],"event":{"name":"CPP '26: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Rennes France","acronym":"CPP '26","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779031.3779109","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T16:54:45Z","timestamp":1775667285000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779031.3779109"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":27,"alternative-id":["10.1145\/3779031.3779109","10.1145\/3779031"],"URL":"https:\/\/doi.org\/10.1145\/3779031.3779109","relation":{},"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}