Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Sun 18 Sep 2016 11:15 - 11:45 at Conference Room 3 - Session 1 (Effects)

Recently we have seen a renewed interest in programming languages that tame the complexity of state and concurrency through refined type systems with more fine-grained control over effects. In addition to simplifying reasoning and eliminating whole classes of bugs, statically controlling effects opens the door to advanced compiler optimisations, such as automatic parallelisation. The flip-side of this refined typing is that these languages often have to include trusted library code that violate the static typing discipline, in ways that are claimed to be unobservable to clients. In this paper we define a logical relation for a language with an ML-like type system refined with effect annotations that supports reasoning about contextual equivalence of potentially ill-typed terms. Using this relation we can formally justify such claims about breaking typing in unobservable ways. The logical relation also supports type-based optimizations, such as automatically parallelizing expressions whose effects are suitably disjoint. The logical relation is defined in Iris, a state-of-the-art higher-order separation logic. This allows us to fall back to a powerful program logic to prove semantic well-typedness in cases where the static typing discipline is too imprecise.

Sun 18 Sep
Times are displayed in time zone: (GMT+09:00) Osaka, Sapporo, Tokyo change

10:45 - 12:15: HOPE - Session 1 (Effects) at Conference Room 3
hope-2016-papers10:45 - 11:15
Fengyun LiuEPFL, Nicolas StuckiEPFL, LAMP, Sandro StuckiEPFL, Nada AminEPFL, Martin OderskyEcole Polytechnique Federale de Lausanne
hope-2016-papers11:15 - 11:45
Morten Krogh-JespersenAarhus University, Kasper SvendsenAarhus University, Lars BirkedalAarhus University, Denmark
hope-2016-papers11:45 - 12:15
Amin Timany, Bart JacobsiMinds - Distrinet, KU Leuven