Abstract
In reasoning about effectful computations, it often suffices to focus on the effect-free parts. We present a package for automatically lifting equations to effects modelled by applicative functors. It exploits properties of the concrete functor thanks to a modular classification based on combinators. We formalise the meta theory and demonstrate the usability of our Isabelle/HOL package with two case studies. This is a first step towards practical reasoning with effectful computations.
Cite
CITATION STYLE
Lochbihler, A., & Schneider, J. (2016). Equational reasoning with applicative functors. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9807 LNCS, pp. 252–273). Springer Verlag. https://doi.org/10.1007/978-3-319-43144-4_16
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
