Name
Abstract | ||
|---|---|---|
In call-by-value languages, some mutually-recursive value 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. 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 (right-to-left) directed into an algorithmic 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/grammatical criterion which let several subtle bugs slip through as the language kept evolving. 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. |
Year | Venue | DocType |
|---|---|---|
2018 | arXiv: Programming Languages | Journal |
Volume | Citations | PageRank |
abs/1811.08134 | 0 | 0.34 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alban Reynaud | 1 | 0 | 0.68 |
| Gabriel Scherer | 2 | 13 | 4.82 |
| Jeremy Yallop | 3 | 3 | 2.79 |