{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:53:10Z","timestamp":1781855590252,"version":"3.54.5"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"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":[[2021,1,4]]},"abstract":"<jats:p>In call-by-value languages, some mutually-recursive definitions can be safely evaluated to build recursive functions or cyclic data structures, but some definitions (let rec x = x + 1) contain vicious circles and their evaluation fails at runtime. We propose a new static analysis to check the absence of such runtime failures.<\/jats:p>\n                  <jats:p>We present a set of declarative inference rules, prove its soundness with respect to the reference source-level semantics of Nordlander, Carlsson, and Gill [2008], and show that it can be directed into an algorithmic backwards analysis check in a surprisingly simple way.<\/jats:p>\n                  <jats:p>Our implementation of this new check replaced the existing check used by the OCaml programming language, a fragile syntactic criterion which let several subtle bugs slip through as the language kept evolving. We document some issues that arise when advanced features of a real-world functional language (exceptions in first-class modules, GADTs, etc.) interact with safety checking for recursive definitions.<\/jats:p>","DOI":"10.1145\/3434326","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A practical mode system for recursive definitions"],"prefix":"10.1145","volume":"5","author":[{"given":"Alban","family":"Reynaud","sequence":"first","affiliation":[{"name":"ENS Lyon, 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, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jeremy","family":"Yallop","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Andreas Abel and Jean-Philippe Bernardy. 2020. A Unified View of Modalities in Type Systems. In ICFP.","DOI":"10.1145\/3408972"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Beniamino Accattoli. 2013. Evaluating functions as processes. In TERMGRAPH.","DOI":"10.4204\/EPTCS.110.6"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Beniamino Accattoli and Delia Kesner. 2010. The structural lambda-calculus. (Oct. 2010 ). working paper or preprint.","DOI":"10.1007\/978-3-642-15205-4_30"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002724"},{"key":"e_1_2_1_5_1","unstructured":"Romain Bardou. 2005. Typage des modules r\u00e9cursifs en Caml. Technical Report. ENS Lyon."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45309-1_18"},{"key":"e_1_2_1_7_1","first-page":"61","article-title":"Recursion in the call-by-value lambda-calculus","author":"Boudol G\u00e9rard","year":"2002","unstructured":"G\u00e9rard Boudol and Pascal Zimmer. 2002. Recursion in the call-by-value lambda-calculus. In FICS. 61-66.","journal-title":"FICS."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Fr\u00e9d\u00e9ric Bour Thomas Refis and Gabriel Scherer. 2018. Merlin: a language server for OCaml (experience report). PACMPL 2 ICFP ( 2018 ).","DOI":"10.1145\/3236798"},{"key":"e_1_2_1_9_1","volume-title":"ESOP (Lecture Notes in Computer Science","author":"Chang Stephen","unstructured":"Stephen Chang and Matthias Felleisen. 2012. The Call-by-Need Lambda Calculus, Revisited. In ESOP (Lecture Notes in Computer Science, Vol. 7211 ), Helmut Seidl (Ed.). Springer, 128-147."},{"key":"e_1_2_1_10_1","first-page":"293","article-title":"A Type System for Well-founded Recursion. In POPL. ACM, New York","author":"Dreyer Derek","year":"2004","unstructured":"Derek Dreyer. 2004. A Type System for Well-founded Recursion. In POPL. ACM, New York, NY, USA, 293-305.","journal-title":"NY, USA"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Matthias Felleisen and Robert Hieb. 1992. The Revised Report on the Syntactic Theories of Sequential Control and State. Theor. Comput. Sci. 103 2 ( 1992 ) 235-271.","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_1_12_1","first-page":"257","article-title":"Ambivalent Types for Principal Type Inference with GADTs","author":"Garrigue Jacques","year":"2013","unstructured":"Jacques Garrigue and Didier R\u00e9my. 2013. Ambivalent Types for Principal Type Inference with GADTs. In APLAS. 257-272.","journal-title":"APLAS."},{"key":"e_1_2_1_13_1","first-page":"229","volume-title":"Portgual","author":"Genaim Samir","year":"2001","unstructured":"Samir Genaim and Michael Codish. 2001. Inferring termination conditions for logic programs using backwards analysis. In APPIA-GULP-PRODE 2001: Joint Conference on Declarative Programming, \u00c9vora, Portgual, September 26-28, 2001, Proceedings, \u00c9vora, Portugal, September 26-28, 2001, Lu\u00eds Moniz Pereira and Paulo Quaresma (Eds.). Departamento de Inform\u00e1tica, Universidade de \u00c9vora, 229-243."},{"key":"e_1_2_1_14_1","volume-title":"Scheme Workshop.","author":"Ghuloum Abdulaziz","unstructured":"Abdulaziz Ghuloum and R. Kent Dybvig. 2009. Fixing Letrec (reloaded). In Scheme Workshop."},{"key":"e_1_2_1_15_1","unstructured":"Tom Hirschowitz and Sergue\u00ef Lenglet. 2005. A practical type system for generalized recursion. Technical Report. ENS Lyon."},{"key":"e_1_2_1_16_1","first-page":"160","article-title":"Compilation of Extended Recursion in Call-by-value Functional Languages. In PPDP. ACM, New York","author":"Hirschowitz Tom","year":"2003","unstructured":"Tom Hirschowitz, Xavier Leroy, and J. B. Wells. 2003. Compilation of Extended Recursion in Call-by-value Functional Languages. In PPDP. ACM, New York, NY, USA, 160-171.","journal-title":"NY, USA"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-009-9042-z"},{"key":"e_1_2_1_18_1","unstructured":"John Hughes. 1987. Backwards Analysis of Functional Programs. In Partial Evaluation and Mixed Computation."},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Jean-Baptiste Jeannin Dexter Kozen and Alexandra Silva. 2017. CoCaml: Functional Programming with Regular Coinductive Types. Fundamenta Informaticae 150 ( 2017 ) 347-377.","DOI":"10.3233\/FI-2017-1473"},{"key":"e_1_2_1_20_1","first-page":"86","article-title":"The Design and Implementation of BER MetaOCaml-System Description","author":"Kiselyov Oleg","year":"2014","unstructured":"Oleg Kiselyov. 2014. The Design and Implementation of BER MetaOCaml-System Description. In FLOPS. 86-102.","journal-title":"FLOPS."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/575336"},{"key":"e_1_2_1_23_1","volume-title":"Unrestricted Pure Call-by-value Recursion. In ML Workshop.","author":"Nordlander Johan","unstructured":"Johan Nordlander, Magnus Carlsson, and Andy J. Gill. 2008. Unrestricted Pure Call-by-value Recursion. In ML Workshop."},{"key":"e_1_2_1_24_1","unstructured":"Ilya Sergey Simon Peyton-Jones and Dimitrios Vytiniotis. 2017a. Theory and Practice of Demand Analysis in Haskell. draft."},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Ilya Sergey Dimitrios Vytiniotis Simon L. Peyton Jones and Joachim Breitner. 2017b. Modular higher order cardinality analysis in theory and practice. J. Funct. Program. 27 ( 2017 ) e11.","DOI":"10.1017\/S0956796817000016"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990074"},{"key":"e_1_2_1_27_1","unstructured":"Don Syme. 2005. An Alternative Approach to Initializing Mutually Referential Objects. Technical Report MSR-TR-2005-31. 27 pages."},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Don Syme. 2006. Initializing Mutually Referential Abstract Objects: The Value Recursion Challenge. Electron. Notes Theor. Comput. Sci. 148 2 ( 2006 ) 3-25.","DOI":"10.1016\/j.entcs.2005.11.038"},{"issue":"0","key":"e_1_2_1_29_1","first-page":"4","article-title":"The Fsharp language reference","volume":"2","author":"Syme Don","year":"2012","unstructured":"Don Syme. 2012. The Fsharp language reference, Versions 2.0 to 4.1, Section 14.6.6, Recursive Safety Analysis.","journal-title":"Versions"},{"key":"e_1_2_1_30_1","volume-title":"Fixing Letrec: A Faithful Yet Eficient Implementation of Scheme's Recursive Binding Construct. Journal of Higher-Order and Symbolic Computation 18 ( 2005 ).","author":"Waddell Oscar","year":"2005","unstructured":"Oscar Waddell, Dipanwita Sarkar, and R. Kent Dybving. 2005. Fixing Letrec: A Faithful Yet Eficient Implementation of Scheme's Recursive Binding Construct. Journal of Higher-Order and Symbolic Computation 18 ( 2005 )."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434326","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434326","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:25:39Z","timestamp":1781853939000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434326"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":30,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434326"],"URL":"https:\/\/doi.org\/10.1145\/3434326","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}