{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T08:58:42Z","timestamp":1790413122164,"version":"4.1.0"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T00:00:00Z","timestamp":1786924800000},"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,8,17]]},"abstract":"<jats:p>\n                    OxCaml extends the OCaml type system with support for safe low-level systems programming via\n                    <jats:italic toggle=\"yes\">modes<\/jats:italic>\n                    . For example, OxCaml's modal\n                    <jats:italic toggle=\"yes\">portability<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">contention<\/jats:italic>\n                    axes ensure that concurrent OxCaml programs have no data races. In practice, however, mode tracking can reject programs that are obviously safe, such as when the data shared across threads is immutable. To remedy this problem, we introduce\n                    <jats:italic toggle=\"yes\">mode crossing<\/jats:italic>\n                    \u2014the ability to automatically strengthen modes (e.g., from\n                    <jats:monospace>nonportable<\/jats:monospace>\n                    to\n                    <jats:monospace>portable<\/jats:monospace>\n                    ) for values of certain types. Mode crossing significantly reduces the annotation burden associated with modal types, and we further introduce a new type system feature,\n                    <jats:italic toggle=\"yes\">modal kinds<\/jats:italic>\n                    .\n                  <\/jats:p>\n                  <jats:p>We present a type-theoretic account of modal kinds, interpret them as monotone functions on a lattice of modes, and extend this interpretation to incorporate abstract types. We verify soundness of the modal kind system in Rocq on top of Iris. We design an inference procedure that reduces kind checking and subsumption to constraints solved by a dedicated lattice solver. Our design is implemented in a large industrial codebase, demonstrating practical usability.<\/jats:p>","DOI":"10.1145\/3828681","type":"journal-article","created":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T20:23:46Z","timestamp":1786998226000},"page":"236-266","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Mode Crossing"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-3193-6940","authenticated-orcid":false,"given":"Benjamin","family":"Peters","sequence":"first","affiliation":[{"name":"MPI-SWS, Saarland Informatics Campus, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1976-3182","authenticated-orcid":false,"given":"Jules","family":"Jacobs","sequence":"additional","affiliation":[{"name":"Jane Street, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-8135-6630","authenticated-orcid":false,"given":"Diana","family":"Kalinichenko","sequence":"additional","affiliation":[{"name":"Jane Street, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-8651-8350","authenticated-orcid":false,"given":"Liam","family":"Stevenson","sequence":"additional","affiliation":[{"name":"Jane Street, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-4883-2707","authenticated-orcid":false,"given":"Aspen","family":"Smith","sequence":"additional","affiliation":[{"name":"Jane Street, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3884-6867","authenticated-orcid":false,"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarland Informatics Campus, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7669-9781","authenticated-orcid":false,"given":"Richard A.","family":"Eisenberg","sequence":"additional","affiliation":[{"name":"Jane Street, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,8,17]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0048939"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/b139095"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_1_5_2","unstructured":"Stephen Dolan. 2019. Unboxed types for OCaml. Jane Street Tech Talk. https:\/\/www.janestreet.com\/tech-talks\/unboxed-types-for-ocaml\/"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","unstructured":"Paul Downen Zena M Ariola Simon Peyton Jones and Richard A Eisenberg. 2020. Kinds are calling conventions. In ICFP. doi:10.1145\/3408986","DOI":"10.1145\/3408986"},{"key":"e_1_3_1_7_2","unstructured":"Richard A Eisenberg Stephen Dolan and Leo White. 2022. Unboxed types for OCaml. In ML Workshop. https:\/\/icfp22.sigplan.org\/details\/mlfamilyworkshop-2022-papers\/13\/Unboxed-types-for-OCaml"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","unstructured":"Richard A Eisenberg and Simon Peyton Jones. 2017. Levity polymorphism. In PLDI. doi:10.1145\/3062341.3062357","DOI":"10.1145\/3062341.3062357"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-12096-2"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","unstructured":"Jeffrey S Foster Manuel F\u00e4hndrich and Alexander Aiken. 1999. A theory of type qualifiers. In PLDI. doi:10.1145\/301618.301665","DOI":"10.1145\/301618.301665"},{"key":"e_1_3_1_11_2","unstructured":"Alain Frisch and Jacques Garrigue. 2010. First-class modules and composable signatures in Objective Caml 3.12. In ACM SIGPLAN Workshop on ML. Baltimore MD."},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704859"},{"key":"e_1_3_1_13_2","unstructured":"Jane Street. 2026. OCaml.org Website. (accessed February 2 2026). https:\/\/ocaml.org\/"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung David Swasey Filip Sieczkowski Kasper Svendsen Aaron Turon Lars Birkedal and Derek Dreyer. 2015. Iris: Monads and invariants as an orthogonal basis for concurrent reasoning. In POPL. doi:10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3674642"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428222"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","unstructured":"Shin-ichi Minato. 1993. Zero-suppressed BDDs for set manipulation in combinatorial problems. In DAC. doi:10.1145\/157485.164890","DOI":"10.1145\/157485.164890"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","unstructured":"Matthew W Papi Mahmood Ali Telmo Luis Correa Jr. Jeff H Perkins and Michael D Ernst. 2008. Practical pluggable types for Java. In ISSTA. doi:10.1145\/1390630.1390656","DOI":"10.1145\/1390630.1390656"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","unstructured":"Benjamin Peters Jules Jacobs Diana Kalinichenko Liam Stevenson Aspen Smith Derek Dreyer and Richard A Eisenberg. 2026. Artifact for \u201cMode Crossing\u201d. Zenodo. doi:10.5281\/zenodo.20272263","DOI":"10.5281\/zenodo.20272263"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632866"},{"key":"e_1_3_1_24_2","unstructured":"The Rust Project Developers. 2026. Coinduction. Rust Compiler Development Guide. https:\/\/rustc-dev-guide.rust-lang.org\/solve\/coinduction.html"},{"key":"e_1_3_1_25_2","unstructured":"The Rust Project Developers. 2026. Send and Sync. The Rustonomicon. https:\/\/doc.rust-lang.org\/nomicon\/send-and-sync.html"},{"key":"e_1_3_1_26_2","unstructured":"The Swift Project Authors. 2026. The Swift Programming Language: Concurrency. Swift.org Documentation. https:\/\/docs.swift.org\/swift-book\/documentation\/the-swift-programming-language\/concurrency\/"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3776644"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3828681","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T08:11:53Z","timestamp":1790410313000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3828681"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,8,17]]},"references-count":26,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2026,8,17]]}},"alternative-id":["10.1145\/3828681"],"URL":"https:\/\/doi.org\/10.1145\/3828681","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,8,17]]},"assertion":[{"value":"2026-02-19","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-05-13","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-08-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}