Congress detail

Authors: Kenji Maillard; Danel Ahman; Robert Atkey; Guido Martínez; Catalin Hritcu; Exequiel Rivas; Éric Tanter.

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

Link: here