Authors: Kenji Maillard; Danel Ahman; Robert Atkey; Guido Martínez; Catalin Hritcu; Exequiel Rivas; Éric Tanter.
Title: Dijkstra Monads for All.
Resumen: This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effectsusing Dijkstra monads, which we define as monad-like structures indexed by a specification monad. We provethat any monad morphism between a computational monad and a specification monad gives rise to a Dijkstramonad, which provides great flexibility for obtaining Dijkstra monads tailored to the verification task athand. We moreover show that a large variety of specification monads can be obtained by applying monadtransformers to various base specification monads, including predicate transformers and Hoare-style prevand postconditions. For defining correct monad transformers, we propose a language inspired by Moggi?smonadic metalanguage that is parameterized by a dependent type theory. We also develop a notion of algebraicoperations for Dijkstra monads, and start to investigate two ways of also accommodating effect handlers. Weimplement our framework in both Coq and F*, and illustrate that it supports a wide variety of verificationstyles for effects such as exceptions, nondeterminism, state, input-output, and general recursion.
Meeting type: Conferencia.
Type of job: Artículo Completo.
Production: Dijkstra Monads for All.
Scientific meeting: International Conference on Functional Programming.
Meeting place: Berlín.
Organizing Institution: ACM-SIGPLAN.
It's published?: Yes
Publication place: Nueva York
Meeting month: 8