Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Thu 22 Aug 2019 10:30 - 10:55 at Pine - Session 2 Chair(s): Andreas Rossberg

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 Aug

10:30 - 12:00: ML 2019 - Session 2 at Pine
Chair(s): Andreas RossbergDfinity
mlfamilyworkshop-2019-papers10:30 - 10:55
Alban ReynaudENS Lyon, Gabriel SchererINRIA Saclay, Jeremy YallopUniversity of Cambridge, UK
mlfamilyworkshop-2019-papers10:55 - 11:20
Oleg Kiselyov, Jeremy YallopUniversity of Cambridge, UK
mlfamilyworkshop-2019-papers11:20 - 11:45
Frank EmrichThe University of Edinburgh, Sam LindleyThe University of Edinburgh and Imperial College London, Jan StolarekUniversity of Edinburgh, UK, James CheneyUniversity of Edinburgh, UK