Extending Equational Monadic Reasoning with Monad Transformers

Affeldt, Reynald; Nowak, David

Document type :

Communication dans un congrès avec actes

DOI :

10.4230/LIPIcs.TYPES.2020.2

Title :

Extending Equational Monadic Reasoning with Monad Transformers

Author(s) :

Affeldt, Reynald [Auteur]
National Institute of Advanced Industrial Science and Technology [AIST]
Nowak, David [Auteur]

Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]

Conference title :

26th International Conference on Types for Proofs and Programs, TYPES 2020

City :

Turin

Country :

Italie

Start date of the conference :

2020-03-02

Journal title :

LIPIcs

Publication date :

2021-06-07

HAL domain(s) :

Informatique [cs]/Logique en informatique [cs.LO]

English abstract : [en]

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 ...
Show more >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 with a non-standard use of Coq that combines impredicative polymorphism and parametricity.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

Collections :

Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL

Files

http://arxiv.org/pdf/2011.03463
Open access
Access the document

Extending Equational Monadic Reasoning ... BibTeX CSV Excel RIS

Files

Extending Equational Monadic Reasoning ...

BibTeX

CSV

Excel

RIS