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í