2018/11/30 by Alban Reynaud, Gabriel Scherer, Jeremy Yallop · 2 citations
Computer Science · #Artificial intelligence #Class (philosophy) #Computer science #Formal Methods in Verification #Functional programming #Inference #Lazy evaluation #Logic, programming, and type systems #Programming language #Semantics (computer science) #Set (abstract data type) #Software Engineering Research #Soundness #Static analysis #Theoretical computer science #Type inference #cs.PL
paper · pdf · doi:10.1145/3434326
published in Proceedings of the ACM on Programming Languages 5(POPL), 1-29 (Association for Computing Machinery) · Author version of POPL'21 article. 29 pages + Appendices
arxiv created 2020/12/23 · arxiv updated 2020/12/24 · openalex publication_date 2021/01/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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. 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. 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.