{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:10:23Z","timestamp":1784196623860,"version":"3.55.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,8,5]]},"abstract":"<jats:p>\n                    We present a novel characterization of stable mergesort functions using relational parametricity, and show that it implies the functional correctness of mergesort. As a result, one can prove the correctness of several variations of mergesort (\n                    <jats:italic toggle=\"yes\">e.g<\/jats:italic>\n                    ., top-down, bottom-up, tail-recursive, non-tail-recursive, smooth, and non-smooth mergesorts) by proving the characteristic property for each variation. Thanks to our characterization and the parametricity translation, we deduced the correctness results, including stability, of various implementations of mergesort for lists, including highly optimized ones, in the\n                    <jats:sc>Rocq<\/jats:sc>\n                    Prover (formerly the\n                    <jats:sc>Coq<\/jats:sc>\n                    Proof Assistant).\n                  <\/jats:p>","DOI":"10.1145\/3747505","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3540-1050","authenticated-orcid":false,"given":"Cyril","family":"Cohen","sequence":"first","affiliation":[{"name":"Inria, CNRS, ENS de Lyon, Universit\u00e9 Claude Bernard Lyon 1, LIP, UMR 5668, Lyon, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1855-5189","authenticated-orcid":false,"given":"Kazuhiko","family":"Sakaguchi","sequence":"additional","affiliation":[{"name":"CNRS, ENS de Lyon, Universit\u00e9 Claude Bernard Lyon 1, LIP, UMR 5668, Lyon, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632920"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_8"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_6"},{"key":"e_1_3_2_6_1","unstructured":"cbrt-x. 2023. haskell\/core-libraries-committee#236: Improve performance of Data.List.sort. https:\/\/github.com\/haskell\/core-libraries-committee\/issues\/236 Accessed: 2025-02-21."},{"key":"e_1_3_2_7_1","volume-title":"Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala Adam","year":"2013","unstructured":"Adam Chlipala. 2013. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press. http:\/\/mitpress.mit.edu\/books\/certified-programming-dependent-types"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Cyril Cohen and Kazuhiko Sakaguchi. 2025. Stable sort algorithms and their stability proofs in Rocq. doi:10.5281\/zenodo.15848446","DOI":"10.5281\/zenodo.15848446"},{"key":"e_1_3_2_9_1","volume-title":"Proc. of the 1999 Haskell Workshop","author":"Day Nancy A.","year":"1999","unstructured":"Nancy A. Day, John Launchbury, and Jeff Lewis. 1999. Logical Abstractions in Haskell. In Proc. of the 1999 Haskell Workshop. https:\/\/www.haskell.org\/haskell-symposium\/1999\/1999-28.pdf Technical Report UU-CS-1999-28, Utrecht University."},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9426-4"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(82)90016-8"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7_3"},{"key":"e_1_3_2_13_1","unstructured":"Georges Gonthier. 2009. RE: [Coq-Club] Sorting. https:\/\/sympa.inria.fr\/sympa\/arc\/coq-club\/2009-04\/msg00040.html Accessed: 2021-11-11."},{"key":"e_1_3_2_14_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","year":"2022","unstructured":"Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2022. Introduction to Algorithms (fourth ed.). MIT Press. https:\/\/mitpress.mit.edu\/9780262046305\/"},{"key":"e_1_3_2_15_1","unstructured":"Hugo Herbelin. 2009. Addition of mergesort + cleaning of the Sorting library. https:\/\/github.com\/coq\/coq\/commit\/f698148f6aee01a207ce5ddd4bebf19da2108bff Accessed: 2025-02-13."},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364394.2364405"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40355-2_11"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498726"},{"key":"e_1_3_2_19_1","unstructured":"Jane Street Group LLC. 2024. Core: Industrial strength alternative to OCaml\u2019s standard library. https:\/\/ocaml.org\/p\/core\/v0.17.1\/doc\/Core\/index.html Accessed: 2025-02-21 Version 0.17.1."},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290315"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2012.381"},{"key":"e_1_3_2_22_1","unstructured":"Chantal Keller Marc Lasson Abhishek Anand Pierre Roux Emilio Jes\u00fas Gallego Arias Cyril Cohen and Matthieu Sozeau. 2014. Paramcoq: Coq plugin for parametricity. https:\/\/github.com\/coq-community\/paramcoq Accessed: 2024-01-17."},{"key":"e_1_3_2_23_1","volume-title":"The Art of Computer Programming, Volume III: Sorting and Searching","author":"Knuth Donald E.","year":"1973","unstructured":"Donald E. Knuth. 1973. The Art of Computer Programming, Volume III: Sorting and Searching. Addison-Wesley."},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814571"},{"key":"e_1_3_2_25_1","unstructured":"Xavier Leroy. [n.d.]. Library Mergesort. https:\/\/xavierleroy.org\/coq\/Mergesort.html Accessed: 2024-02-10."},{"key":"e_1_3_2_26_1","unstructured":"Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2024. The OCaml system. https:\/\/v2.ocaml.org\/releases\/4.14\/htmlman\/Accessed: 2024-02-10 Version 4.14."},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7118596"},{"key":"e_1_3_2_28_1","unstructured":"Tobias Nipkow Jasmin Blanchette Manuel Eberl Alejandro Gomez-Londono Peter Lammich Christian Sternagel Simon Wimmer and Bohua Zhan. 2025. Functional Data Structures and Algorithms: A Proof Assistant Approach. https:\/\/functional-algorithms-verified.org\/ Accessed: 2025-06-13."},{"key":"e_1_3_2_29_1","volume-title":"A smooth applicative merge sort","author":"O\u2019Keefe Richard A.","year":"1982","unstructured":"Richard A. O\u2019Keefe. 1982. A smooth applicative merge sort. Department of Artificial Intelligence, University of Edinburgh. This literature does not seem available at the point of writing the present paper. Therefore, when we refer to it, we actually rather refer to the part of Paulson [1996] explaining the ideas of this literatures."},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611972863.16"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/524580"},{"key":"e_1_3_2_32_1","unstructured":"Uday S. Reddy. 1997. When Parametricity implies Naturality (Notes). (1997). https:\/\/citeseerx.ist.psu.edu\/pdf\/c54b8f6633e2ad8a55195ba24ffae1e3d377407a Accessed: 2025-02-12."},{"key":"e_1_3_2_33_1","first-page":"513","volume-title":"Proc. of the IFIP 9th World Computer Congress (IFIP\u201983)","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In Proc. of the IFIP 9th World Computer Congress (IFIP\u201983). North-Holland\/IFIP, 513\u2013523."},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9260-7"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2019.29"},{"key":"e_1_3_2_36_1","unstructured":"The GHC Team. 2024a. Glasgow Haskell Compiler User\u2019s Guide. https:\/\/downloads.haskell.org\/~ghc\/9.8.4\/docs\/users_guide\/Accessed: 2025-02-21 Version 9.8.4."},{"key":"e_1_3_2_37_1","unstructured":"The GHC Team. 2024b. Glasgow Haskell Compiler User\u2019s Guide. https:\/\/downloads.haskell.org\/~ghc\/9.12.1\/docs\/users_guide\/Accessed: 2025-02-21 Version 9.12.1."},{"key":"e_1_3_2_38_1","unstructured":"The Rocq Development Team. 2025a. The Rocq Reference Manual. https:\/\/rocq-prover.org\/doc\/V9.0.0\/refman\/ the PDF version with numbered sections is available at https:\/\/github.com\/coq\/coq\/releases\/tag\/V9.0.0."},{"key":"e_1_3_2_39_1","unstructured":"The Rocq Development Team. 2025b. Section 2.1.11 \u201cSections\u201d. In [The Rocq Development Team 2025a]. https:\/\/rocq-prover.org\/doc\/V9.0.0\/refman\/language\/core\/sections.html"},{"key":"e_1_3_2_40_1","unstructured":"The Rocq Development Team. 2025c. Section 2.1.12 \u201cThe Module System\u201d. In [The Rocq Development Team 2025a]. https:\/\/rocq-prover.org\/doc\/V9.0.0\/refman\/language\/core\/modules.html"},{"key":"e_1_3_2_41_1","unstructured":"The Rocq Development Team. 2025d. Section 2.1.9 \u201cInductive types and recursive functions\u201d. In [The Rocq Development Team 2025a]. https:\/\/rocq-prover.org\/doc\/V9.0.0\/refman\/language\/core\/inductive.html"},{"key":"e_1_3_2_42_1","unstructured":"The Rocq Development Team. 2025e. Section 2.2.6 \u201cImplicit Coercions\u201d. In [The Rocq Development Team 2025a]. https:\/\/rocq-prover.org\/doc\/V9.0.0\/refman\/addendum\/implicit-coercions.html"},{"key":"e_1_3_2_43_1","unstructured":"The Rocq Development Team. 2025f. Section 4.1.1 \u201cThe Coq libraries\u201d. In [The Rocq Development Team 2025a]. https:\/\/rocq-prover.org\/doc\/V9.0.0\/refman\/language\/coq-library.html"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328445"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_3_2_46_1","unstructured":"Philip Wadler. 1990. Recursive types for free! https:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/free-rectypes\/free-rectypes.txt Accessed: 2025-01-29."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747505","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:01:51Z","timestamp":1784196111000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747505"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":45,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747505"],"URL":"https:\/\/doi.org\/10.1145\/3747505","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"2025-02-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}