{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:40:56Z","timestamp":1780994456448,"version":"3.54.1"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    We present\n                    <jats:sc>ZipML<\/jats:sc>\n                    , a new path-based type system for a fully fledged ML-module language that avoids the signature avoidance problem. This is achieved by introducing\n                    <jats:italic toggle=\"yes\">floating fields<\/jats:italic>\n                    , which act as additional fields of a signature, invisible to the user but still accessible to the typechecker. In practice, they are handled as\n                    <jats:italic toggle=\"yes\">zippers<\/jats:italic>\n                    on signatures, and can be seen as a lightweight extension of existing signatures. Floating fields allow to delay the resolution of instances of the signature avoidance problem as long as possible or desired. Since they do not exist at runtime, they can be simplified along type equivalence, and dropped once they became unreachable. We give rewriting rules for the simplification of floating fields without loss of type-sharing and present an algorithm that implements them. Remaining floating fields may fully disappear at signature ascription, especially in the presence of toplevel interfaces. Residual unavoidable floating fields can be shown to the user as a last resort, improving the quality of error messages. Besides,\n                    <jats:sc>ZipML<\/jats:sc>\n                    implements early and lazy strengthening, as well as lazy inlining of definitions, preventing duplication of signatures inside the typechecker. The correctness of the type system is proved by elaboration into M\n                    <jats:sup>\n                      <jats:italic toggle=\"yes\">\u03c9<\/jats:italic>\n                    <\/jats:sup>\n                    , which has itself been proved sound by translation to F\n                    <jats:sup>\n                      <jats:italic toggle=\"yes\">\u03c9<\/jats:italic>\n                    <\/jats:sup>\n                    .\n                    <jats:sc>ZipML<\/jats:sc>\n                    has been designed to be an improvement over\n                    <jats:sc>OCaml<\/jats:sc>\n                    that could be retrofitted into the existing implementation.\n                  <\/jats:p>","DOI":"10.1145\/3704902","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1962-1991","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Avoiding Signature Avoidance in ML Modules with Zippers"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6333-6092","authenticated-orcid":false,"given":"Cl\u00e9ment","family":"Blaudeau","sequence":"first","affiliation":[{"name":"Inria, Paris, France"},{"name":"Universit\u00e9 de Paris Cit\u00e9, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0693-6278","authenticated-orcid":false,"given":"Didier","family":"R\u00e9my","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2107-7678","authenticated-orcid":false,"given":"Gabriel","family":"Radanne","sequence":"additional","affiliation":[{"name":"Inria, Lyon, France"},{"name":"EnsL, Lyon, France"},{"name":"UCBL, Lyon, France"},{"name":"CNRS, Lyon, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199478"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649818"},{"key":"e_1_3_2_4_2","first-page":"479","volume-title":"Proceedings IFIP TC2 working conference on programming concepts and methods","author":"Cardelli Luca","year":"1990","unstructured":"Luca Cardelli and Xavier Leroy. 1990. Abstract types and the dot notation. In Proceedings IFIP TC2 working conference on programming concepts and methods. North-Holland, 479\u2013504."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009892"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000222"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006429"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604151"},{"key":"e_1_3_2_9_2","unstructured":"Jacques Guarrigue and Leo White. 2014. Type-level module aliases: independent and equal (ML Family\/OCaml Users and Developers workshops). https:\/\/www.math.nagoya-u.ac.jp\/~garrigue\/papers\/modalias.pdf"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176927"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96744"},{"key":"e_1_3_2_12_2","doi-asserted-by":"crossref","unstructured":"Robert Harper and Christopher A. Stone. 2000. A type-theoretic interpretation of standard ML. In Proof Language and Interaction. https:\/\/api.semanticscholar.org\/CorpusID:9208816","DOI":"10.7551\/mitpress\/5641.003.0019"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002864"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176926"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199476"},{"key":"e_1_3_2_16_2","unstructured":"Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my Kc Sivaramakrishnan and J\u00e9r\u00f4me Vouillon. 2023. The OCaml system release 5.1: Documentation and user\u2019s manual. Intern report. Inria. https:\/\/inria.hal.science\/hal-00930213"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Runhang Li and Jeremy Yallop. 2017. Extending OCaml\u2019s\u2019open\u2019. In Proceedings ML Family \/ OCaml Users and Developers workshops ML\/OCaml 2017 Oxford UK 7th September 2017 (EPTCS Vol. 294) Sam Lindley and Gabriel Scherer (Eds.). 1\u201314. https:\/\/doi.org\/10.4204\/EPTCS.294.1 10.4204\/EPTCS.294.1","DOI":"10.4204\/EPTCS.294.1"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3386336"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512670"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451167"},{"key":"e_1_3_2_21_2","volume-title":"The Definition of Standard ML (revised)","author":"Milner Robin","year":"1990","unstructured":"Robin Milner, Mads Tofte, and Robert Harper. 1990. The Definition of Standard ML (revised). MIT Press, Cambridge, MA, USA."},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2319.003.0001"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318606"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/1160074.1159813"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2005.11.045"},{"key":"e_1_3_2_26_2","unstructured":"Andreas Rossberg. 1999. Undecidability of OCaml type checking. https:\/\/sympa.inria.fr\/sympa\/arc\/caml-list\/1999-07\/msg00027.html."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000205"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2450136.2450137"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46425-5_22"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/507669.507644"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82621-0"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317801"},{"key":"e_1_3_2_34_2","unstructured":"Leo White. 2015. Girard Paradox implemented in OCaml using abstract signatures. Retrieved December 13 2024 from https:\/\/archive.softwareheritage.org\/swh:1:dir:4fdeca3fd7e9a4f080ab8c191522176db1de5b76;origin=https:\/\/github.com\/lpw25\/girards-paradox;visit=swh:1:snp:884b4fac22a378aa8493c83ff967f29bcb0b11d2;anchor=swh:1:rev: 17ccd5d325bf338721478ad1d8ef8f88cf1389fa"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704902","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704902","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:43Z","timestamp":1770200263000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704902"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":33,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704902"],"URL":"https:\/\/doi.org\/10.1145\/3704902","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}