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.ITP.2021.29
URN: urn:nbn:de:0030-drops-139241
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13924/
Nigron, Pierre ;
Dagand, Pierre-Évariste
Reaching for the Star: Tale of a Monad in Coq
Abstract
Monadic programming is an essential component in the toolbox of functional programmers. For the pure and total programmers, who sometimes navigate the waters of certified programming in type theory, it is the only means to concisely implement the imperative traits of certain algorithms. Monads open up a portal to the imperative world, all that from the comfort of the functional world. The trend towards certified programming within type theory begs the question of reasoning about such programs. Effectful programs being encoded as pure programs in the host type theory, we can readily manipulate these objects through their encoding. In this article, we pursue the idea, popularized by Maillard [Kenji Maillard, 2019], that every monad deserves a dedicated program logic and that, consequently, a proof over a monadic program ought to take place within a Floyd-Hoare logic built for the occasion. We illustrate this vision through a case study on the SimplExpr module of CompCert [Xavier Leroy, 2009], using a separation logic tailored to reason about the freshness of a monadic gensym.
BibTeX - Entry
@InProceedings{nigron_et_al:LIPIcs.ITP.2021.29,
author = {Nigron, Pierre and Dagand, Pierre-\'{E}variste},
title = {{Reaching for the Star: Tale of a Monad in Coq}},
booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)},
pages = {29:1--29:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-188-7},
ISSN = {1868-8969},
year = {2021},
volume = {193},
editor = {Cohen, Liron and Kaliszyk, Cezary},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13924},
URN = {urn:nbn:de:0030-drops-139241},
doi = {10.4230/LIPIcs.ITP.2021.29},
annote = {Keywords: monads, hoare logic, separation logic, Coq}
}
