Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Wed 21 Aug 2019 10:52 - 11:15 at Aurora Borealis - Program Verification Chair(s): Adam Chlipala

This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effects using Dijkstra monads, which we define as monad-like structures indexed by a specification monad. We prove that any monad morphism between a computational monad and a specification monad gives rise to a Dijkstra monad, which provides great flexibility for obtaining Dijkstra monads tailored to the verification task at hand. We moreover show that a large variety of specification monads can be obtained by applying monad transformers to various base specification monads, including predicate transformers and Hoare-style pre- and postconditions. For defining correct monad transformers, we propose a language inspired by Moggi’s monadic metalanguage that is parameterized by a dependent type theory. We also develop a notion of algebraic operations for Dijkstra monads, and start to investigate two ways of also accommodating effect handlers. We implement our framework in both Coq and F*, and illustrate that it supports a wide variety of verification styles for effects such as exceptions, nondeterminism, state, input-output, and general recursion.

Wed 21 Aug

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

10:30 - 12:00
Program VerificationResearch Papers at Aurora Borealis
Chair(s): Adam Chlipala Massachusetts Institute of Technology
10:30
22m
Talk
A predicate transformer semantics for effects (Functional Pearl)
Research Papers
Wouter Swierstra Utrecht University, Netherlands, Tim Baanen Utrecht University
10:52
22m
Talk
Dijkstra Monads for All
Research Papers
Kenji Maillard Inria Paris and ENS Paris, Danel Ahman University of Ljubljana, Robert Atkey University of Strathclyde, Guido Martínez CIFASIS-CONICET, Argentina, Cătălin Hriţcu Inria Paris, Exequiel Rivas Inria Paris, Éric Tanter University of Chile & Inria Paris
Pre-print
11:15
22m
Talk
Mechanized Relational Verification of Concurrent Programs with Continuations
Research Papers
Amin Timany imec-Distrinet KU-Leuven, Lars Birkedal Aarhus University
11:37
22m
Talk
Sequential Programming for Replicated Data Stores
Research Papers
Nicholas V. Lewchenko University of Colorado Boulder, Arjun Radhakrishna Microsoft, Akash Gaonkar , Pavol Cerny University of Colorado Boulder
DOI Pre-print