Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Thu 22 Aug 2019 11:30 - 12:00 at Aurora Borealis - Paper Session 1: Classes & Instances Chair(s): Jose Calderon

In applications with a complex structure of side-effects, effects should be dealt with modularly: components should be programmed against abstract effect interfaces that other components can instantiate as required, and reusable effect patterns should be factored out from the rest of the application. In this paper, we study a new, general approach to achieve this in Haskell by combining effect polymorphism and the recently proposed coherent explicit dictionary applications. We demonstrate the elegance and generality of our approach in μVeriFast: a Haskell-based reimplementation of the semi-automatic separation-logic-based verification tool VeriFast. This implementation features a complex interplay of advanced side-effects: a backtracking search of program paths with angelic and demonic non-determinism, interaction with an underlying off-the-shelf SMT solver, and mutable state that is either backtracked or not during the search. Our use of effect polymorphism improves over the current non-modular implementation of VeriFast, allows us to nicely factor out the backtracking search pattern as a new AssumeAssert monad, and enables advanced features involving effects, such as the non-intrusive addition of a graphical symbolic debugger based on delimited continuations.

Presentation (presentatie.pdf)300KiB

Conference Day
Thu 22 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:00
Paper Session 1: Classes & InstancesHaskell at Aurora Borealis
Chair(s): Jose CalderonGalois, Inc.
Research paper
Bidirectional Type Class Instances
Koen PauwelsKU Leuven, Georgios KarachaliasKU Leuven, Belgium, Michiel DerhaegGuardsquare, Tom SchrijversKU Leuven
Research paper
Generic and Flexible Defaults for Verified, Law-Abiding Type-Class Instances
Ryan ScottIndiana University at Bloomington, USA, Ryan R. NewtonIndiana University
Pre-print File Attached
Research paper
Modular effects in Haskell through effect polymorphism and explicit dictionary applications - A new approach and the μVeriFast verifier as a case study
Dominique DevrieseVrije Universiteit Brussel
File Attached