License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2020.2
URN: urn:nbn:de:0030-drops-138810
URL: https://drops.dagstuhl.de/opus/volltexte/2021/13881/
Go to the corresponding LIPIcs Volume Portal


Affeldt, Reynald ; Nowak, David

Extending Equational Monadic Reasoning with Monad Transformers

pdf-format:
LIPIcs-TYPES-2020-2.pdf (0.9 MB)


Abstract

There is a recent interest for the verification of monadic programs using proof assistants. This line of research raises the question of the integration of monad transformers, a standard technique to combine monads. In this paper, we extend Monae, a Coq library for monadic equational reasoning, with monad transformers and we explain the benefits of this extension. Our starting point is the existing theory of modular monad transformers, which provides a uniform treatment of operations. Using this theory, we simplify the formalization of models in Monae and we propose an approach to support monadic equational reasoning in the presence of monad transformers. We also use Monae to revisit the lifting theorems of modular monad transformers by providing equational proofs and explaining how to patch a known bug using a non-standard use of Coq that combines impredicative polymorphism and parametricity.

BibTeX - Entry

@InProceedings{affeldt_et_al:LIPIcs.TYPES.2020.2,
  author =	{Affeldt, Reynald and Nowak, David},
  title =	{{Extending Equational Monadic Reasoning with Monad Transformers}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{2:1--2:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13881},
  URN =		{urn:nbn:de:0030-drops-138810},
  doi =		{10.4230/LIPIcs.TYPES.2020.2},
  annote =	{Keywords: monads, monad transformers, Coq, impredicativity, parametricity}
}

Keywords: monads, monad transformers, Coq, impredicativity, parametricity
Collection: 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Issue Date: 2021
Date of publication: 07.06.2021
Supplementary Material: Software (Proof Scripts): https://github.com/affeldt-aist/monae/ archived at: https://archive.softwareheritage.org/swh:1:dir:2d68878d365fe72744f8b085fa29df385567f6c9


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI