Detalle del congreso

Autores: 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.

Tipo de reunión: Conferencia.

Tipo de trabajo: Artículo Completo.

Producción: Dijkstra Monads for All.

Reunión científica: International Conference on Functional Programming.

Lugar: Berlín.

Institución organizadora: ACM-SIGPLAN.

Publicado: Sí

Lugar publicación: Nueva York

Mes de reunión: 8

Página web: aquí