Dijkstra monads for all

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

Research output: Contribution to journalArticle

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

Fingerprint

Specifications
Semantics

Keywords

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

Cite this

Maillard, K., Ahman, D., Atkey, R., Martínez, G., Hritcu, C., Rivas, E., & Tanter, É. (2019). Dijkstra monads for all. Proceedings of the ACM on Programming Languages (PACMPL), 3(ICFP), [104]. https://doi.org/10.1145/3341708
Maillard, Kenji ; Ahman, Danel ; Atkey, Robert ; Martínez, Guido ; Hritcu, Catalin ; Rivas, Exequiel ; Tanter, Éric. / Dijkstra monads for all. In: Proceedings of the ACM on Programming Languages (PACMPL). 2019 ; Vol. 3, No. ICFP.
@article{4843fd36de0e47958c6f8ecd138bfc91,
title = "Dijkstra monads for all",
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.",
keywords = "program verification, side-effects, monads, dependent types, programming, computation",
author = "Kenji Maillard and Danel Ahman and Robert Atkey and Guido Mart{\'i}nez and Catalin Hritcu and Exequiel Rivas and {\'E}ric Tanter",
year = "2019",
month = "8",
day = "1",
doi = "10.1145/3341708",
language = "English",
volume = "3",
journal = "Proceedings of the ACM on Programming Languages (PACMPL)",
issn = "2475-1421",
number = "ICFP",

}

Maillard, K, Ahman, D, Atkey, R, Martínez, G, Hritcu, C, Rivas, E & Tanter, É 2019, 'Dijkstra monads for all' Proceedings of the ACM on Programming Languages (PACMPL), vol. 3, no. ICFP, 104. https://doi.org/10.1145/3341708

Dijkstra monads for all. / Maillard, Kenji; Ahman, Danel; Atkey, Robert; Martínez, Guido; Hritcu, Catalin; Rivas, Exequiel; Tanter, Éric.

In: Proceedings of the ACM on Programming Languages (PACMPL), Vol. 3, No. ICFP, 104, 01.08.2019.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Dijkstra monads for all

AU - Maillard, Kenji

AU - Ahman, Danel

AU - Atkey, Robert

AU - Martínez, Guido

AU - Hritcu, Catalin

AU - Rivas, Exequiel

AU - Tanter, Éric

PY - 2019/8/1

Y1 - 2019/8/1

N2 - 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.

AB - 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.

KW - program verification

KW - side-effects

KW - monads

KW - dependent types

KW - programming

KW - computation

U2 - 10.1145/3341708

DO - 10.1145/3341708

M3 - Article

VL - 3

JO - Proceedings of the ACM on Programming Languages (PACMPL)

T2 - Proceedings of the ACM on Programming Languages (PACMPL)

JF - Proceedings of the ACM on Programming Languages (PACMPL)

SN - 2475-1421

IS - ICFP

M1 - 104

ER -

Maillard K, Ahman D, Atkey R, Martínez G, Hritcu C, Rivas E et al. Dijkstra monads for all. Proceedings of the ACM on Programming Languages (PACMPL). 2019 Aug 1;3(ICFP). 104. https://doi.org/10.1145/3341708