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. 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 et al. (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 OCaml, a fragile syntactic/grammatical criterion which let several subtle bugs slip through as the language acquired new features such as GADTs that have subtle interactions with value recursion.
Thu 22 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00
|A right-to-left type system for value recursion
|let (rec) insertion without effects, lights or magic
|(TyDe Presentation) FreezeML: Complete and Easy Type Inference for First-Class Polymorphism