Dijkstra monads for all

Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter

Research output: Contribution to journalArticle

7 Downloads (Pure)

Abstract

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.
Original languageEnglish
Article number104
Number of pages29
JournalProceedings of the ACM on Programming Languages (PACMPL)
Volume3
Issue numberICFP
DOIs
Publication statusPublished - 1 Aug 2019

Keywords

  • program verification
  • side-effects
  • monads
  • dependent types
  • programming
  • computation

Fingerprint Dive into the research topics of 'Dijkstra monads for all'. Together they form a unique fingerprint.

Cite this