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
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:00: ML 2019 - Session 2 at Pine
Chair(s): Andreas RossbergDfinity Stiftung
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