{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T16:09:04Z","timestamp":1787069344314,"version":"3.56.0"},"reference-count":26,"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\/"}],"funder":[{"name":"AJR","award":["JCJC REPRO"],"award-info":[{"award-number":["JCJC REPRO"]}]}],"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>Common functional languages incentivize tail-recursive functions, as opposed to general recursive functions that consume stack space and may not scale to large inputs. This distinction occasionally requires writing functions in a tail-recursive style that may be more complex and slower than the natural, non-tail-recursive definition.<\/jats:p>\n                  <jats:p>\n                    This work describes our implementation of the\n                    <jats:italic toggle=\"yes\">tail modulo constructor<\/jats:italic>\n                    (TMC) transformation in the OCaml compiler, an optimization that provides stack-efficiency for a larger class of functions \u2014 tail-recursive\n                    <jats:italic toggle=\"yes\">modulo constructors<\/jats:italic>\n                    \u2014 which includes in particular the natural definition of\n                    <jats:monospace>List.map<\/jats:monospace>\n                    and many similar recursive data-constructing functions.\n                  <\/jats:p>\n                  <jats:p>\n                    We prove the correctness of this program transformation in a simplified setting \u2014 a small untyped calculus \u2014 that captures the salient aspects of the OCaml implementation. Our proof is mechanized in the\n                    <jats:sc>Coq<\/jats:sc>\n                    proof assistant, using the\n                    <jats:sc>Iris<\/jats:sc>\n                    base logic. An independent contribution of our work is an extension of the Simuliris approach to define simulation relations that support different calling conventions. To our knowledge, this is the first use of\n                    <jats:sc>Simuliris<\/jats:sc>\n                    to prove the correctness of a compiler transformation.\n                  <\/jats:p>","DOI":"10.1145\/3704915","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"2337-2363","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Tail Modulo Cons, OCaml, and Relational Separation Logic"],"prefix":"10.1145","volume":"9","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\/0009-0007-5268-5784","authenticated-orcid":false,"given":"Fr\u00e9d\u00e9ric","family":"Bour","sequence":"additional","affiliation":[{"name":"Tarides, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9126-0937","authenticated-orcid":false,"given":"Basile","family":"Cl\u00e9ment","sequence":"additional","affiliation":[{"name":"OCamlPro, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4069-1235","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","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, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","unstructured":"Cl\u00e9ment Allain. 2024. Tail Modulo Cons OCaml and Relational Separation Logic \u2014 Artifact. https:\/\/doi.org\/10.5281\/zenodo.14103793 10.5281\/zenodo.14103793","DOI":"10.5281\/zenodo.14103793"},{"key":"e_1_3_2_3_1","unstructured":"Thomas Bagrel. 2023. Destination-passing style programming: a Haskell implementation. arXiv:2312.11257 [cs.PL] https:\/\/arxiv.org\/abs\/2312.11257"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837022"},{"key":"e_1_3_2_5_1","volume-title":"JFLA 2021 - Journ\u00e9es Francophones des Langages Applicatifs","author":"Bour Fr\u00e9d\u00e9ric","year":"2021","unstructured":"Fr\u00e9d\u00e9ric Bour, Basile Cl\u00e9ment, and Gabriel Scherer. 2021. Tail Modulo Cons. In JFLA 2021 - Journ\u00e9es Francophones des Langages Applicatifs. Saint M\u00e9dard d\u2019Excideuil, France. https:\/\/inria.hal.science\/hal-03146495"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1034774.1034778"},{"key":"e_1_3_2_7_1","doi-asserted-by":"crossref","unstructured":"Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2021. A separation logic for effect handlers. In POPL. http:\/\/cambium.inria.fr\/~fpottier\/publis\/de-vilhena-pottier-sleh.pdf","DOI":"10.1145\/3410260"},{"key":"e_1_3_2_8_1","doi-asserted-by":"crossref","unstructured":"Klaus Didrich Andreas Fett Carola Gerke Wolfgang Grieskamp and Peter Pepper. 1994. OPAL: Design and implementation of an algebraic programming language. In Programming Languages and System Architectures J\u00fcrg Gutknecht (Ed.).","DOI":"10.1007\/3-540-57840-4_34"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","unstructured":"S\u00e9bastien Doeraene and Peter Van Roy. 2013. A new concurrency model for Scala based on a declarative dataflow core. In Scala Workshop (Montpellier France) (SCALA \u201913). Article 4 10 pages. https:\/\/doi.org\/10.1145\/2489837.2489841 10.1145\/2489837.2489841","DOI":"10.1145\/2489837.2489841"},{"key":"e_1_3_2_10_1","volume-title":"Unwinding stylized recursions into iterations","author":"Friedman Daniel P.","year":"1975","unstructured":"Daniel P. Friedman and David S. Wise. 1975. Unwinding stylized recursions into iterations. Technical Report 19. Computer Science Department, Indiana University, Bloomington. https:\/\/legacy.cs.indiana.edu\/ftp\/techreports\/TR19.pdf"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:9)2021"},{"key":"e_1_3_2_12_1","doi-asserted-by":"crossref","unstructured":"Lennard G\u00e4her Michael Sammler Simon Spies Ralf Jung Hoang-Hai Dang Robbert Krebbers Jeehoon Kang and Derek Dreyer. 2022. Simuliris: a separation logic framework for verifying concurrent program optimizations. (2022).","DOI":"10.1145\/3498689"},{"key":"e_1_3_2_13_1","doi-asserted-by":"crossref","unstructured":"Arma\u00ebl Gu\u00e9neau Johannes Hostert Simon Spies Michael Sammler Lars Birkedal and Derek Dreyer. 2023. Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. In OOPSLA. https:\/\/inria.hal.science\/hal-04203298","DOI":"10.1145\/3622823"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571233"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656398"},{"key":"e_1_3_2_16_1","doi-asserted-by":"crossref","unstructured":"Yasuhiko Minamide. 1998. A functional representation of data structures with a hole. In POPL. https:\/\/sv.c.titech.ac.jp\/minamide\/papers\/hole.popl98.pdf","DOI":"10.1145\/268946.268953"},{"key":"e_1_3_2_17_1","volume-title":"Visions for the Future of Logic Programming: Laying the Foundations for a Modern successor of Prolog","author":"M\u00fcller Martin","year":"1995","unstructured":"Martin M\u00fcller, Tobias M\u00fcller, and Peter Van Roy. 1995. Multi-Paradigm Programming in Oz. In Visions for the Future of Logic Programming: Laying the Foundations for a Modern successor of Prolog. A Workshop in Association with ILPS\u201995."},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211968"},{"key":"e_1_3_2_19_1","volume-title":"REMREC \u2013 A Program for Automatic Recursion Removal in Lisp","author":"Risch Tore","year":"1973","unstructured":"Tore Risch. 1973. REMREC \u2013 A Program for Automatic Recursion Removal in Lisp. Technical Report DLU73\/24. Dept. of Computer Science, Uppsala University. http:\/\/user.it.uu.se\/~torer\/publ\/remrec.pdf"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_24"},{"key":"e_1_3_2_21_1","first-page":"16","volume-title":"ILPS \u201994","author":"Schulte Christian","year":"1994","unstructured":"Christian Schulte and Gert Smolka. 1994. Encapsulated search for higher-order concurrent constraint programming. In ILPS \u201994. MIT Press, 16 pages."},{"key":"e_1_3_2_22_1","doi-asserted-by":"crossref","unstructured":"Jonathan Sobel and Daniel P. Friedman. 1998. Recycling continuations. In ICFP. 251\u2013260. http:\/\/www.cs.indiana.edu\/hyplan\/dfried\/rc.ps","DOI":"10.1145\/289423.289452"},{"key":"e_1_3_2_23_1","doi-asserted-by":"crossref","unstructured":"Simon Spies Lennard G\u00e4her Daniel Gratzer Joseph Tassarotti Robbert Krebbers Derek Dreyer and Lars Birkedal. 2021. Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. In PLDI. https:\/\/iris-project.org\/transfinite-iris\/","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_3_2_24_1","doi-asserted-by":"crossref","unstructured":"Joseph Tassarotti Ralf Jung and Robert Harper. 2017. A Higher-Order Logic for Concurrent Termination-Preserving Refinement. In ESOP. https:\/\/arxiv.org\/abs\/1701.05888","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_3_2_25_1","doi-asserted-by":"crossref","unstructured":"Aaron Turon Derek Dreyer and Lars Birkedal. 2013. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In ICFP. https:\/\/people.mpi-sws.org\/~dreyer\/papers\/caresl\/paper.pdf","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_3_2_26_1","doi-asserted-by":"crossref","unstructured":"Peng Wang Santiago Cuellar and Adam Chlipala. 2014. Compiler verification meets cross-language linking via data abstraction. In OOPSLA. http:\/\/adam.chlipala.net\/papers\/CitoOOPSLA14\/","DOI":"10.1145\/2660193.2660201"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704915","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704915","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:19:01Z","timestamp":1770200341000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704915"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":26,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704915"],"URL":"https:\/\/doi.org\/10.1145\/3704915","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"}}]}}