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
10:30 - 12:00: Research Papers - Program Verification at Aurora Borealis Chair(s): Adam ChlipalaMassachusetts Institute of Technology | ||||||||||||||||||||||||||||||||||||||||||
10:30 - 10:52 Talk | ||||||||||||||||||||||||||||||||||||||||||
10:52 - 11:15 Talk | Kenji MaillardInria Paris and ENS Paris, Danel AhmanUniversity of Ljubljana, Robert AtkeyUniversity of Strathclyde, Guido MartínezCIFASIS-CONICET, Argentina, Cătălin HriţcuInria Paris, Exequiel RivasInria Paris, Éric TanterUniversity of Chile & Inria Paris Pre-print | |||||||||||||||||||||||||||||||||||||||||
11:15 - 11:37 Talk | ||||||||||||||||||||||||||||||||||||||||||
11:37 - 12:00 Talk | Nicholas V. LewchenkoUniversity of Colorado Boulder, Arjun RadhakrishnaMicrosoft, Akash Gaonkar, Pavol CernyUniversity of Colorado Boulder DOI Pre-print |