Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Thu 22 Aug 2019 13:30 - 14:00 at Aurora Borealis - Paper Session 2: Verification Chair(s): Ningning Xie

For the purpose of verifying Haskell programs in Coq, we build on previous work that demonstrates how to reason about existing Haskell programs by translating them into monadic Coq programs. A model of Haskell programs in Coq that is polymorphic over an arbitrary monad is not accepted by Coq’s termination checker. Therefore, instead of a model that is generic over the monad, we use a concrete monad instance, namely the free monad, to model various kinds of effects. This model allows proofs that are generic over the concrete kind of effect.

In this paper we consider implicit effects that may occur in Haskell, namely partiality, errors, and tracing, in detail. We observe that, while proving propositions that hold for all kinds of effects is attractive, not all propositions of interest hold for all kinds of effects. Some propositions fail for certain effects because the common monadic translation models call-by-name and not call-by-need. As modeling call-by-need makes proofs more complex and is not necessary for a variety of effects, we identify a specific class of effects for which we cannot distinguish between call-by-name and call-by-need denotationally. Using this class of effects we can prove propositions for all effects that do not require a model of call-by-need. Besides specifying this class we show how various Haskell language features that are related to implicit effects can be modeled.

Thu 22 Aug

haskellsymp-2019-papers
13:30 - 15:00: Haskell 2019 - Paper Session 2: Verification at Aurora Borealis
Chair(s): Ningning XieThe University of Hong Kong
haskellsymp-2019-papers13:30 - 14:00
Research paper
Jan ChristiansenFlensburg University of Applied Sciences, Germany, Sandra DylusUniversity of Kiel, Germany, Niels BunkenburgUniversity of Kiel, Germany
haskellsymp-2019-papers14:00 - 14:30
Talk
File Attached
haskellsymp-2019-papers14:30 - 15:00
Experience report
Andrey MokhovNewcastle University, UK, Georgy LukyanovNewcastle University, UK, Jakob LechnerRUAG Space Austria GmbH