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

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

13:30 - 15:00
Paper Session 2: VerificationHaskell at Aurora Borealis
Chair(s): Ningning Xie University of Toronto
13:30
30m
Research paper
Verifying Effectful Haskell Programs in Coq
Haskell
Jan Christiansen Flensburg University of Applied Sciences, Germany, Sandra Dylus University of Kiel, Germany, Niels Bunkenburg University of Kiel, Germany
14:00
30m
Talk
Solving Haskell equality constraints using Coq
Haskell
File Attached
14:30
30m
Experience report
Formal Verification of Spacecraft Control Programs: An Experience Report
Haskell
Andrey Mokhov Newcastle University, UK, Georgy Lukyanov Newcastle University, UK, Jakob Lechner RUAG Space Austria GmbH