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: https://drops.dagstuhl.de/opus/volltexte/2021/13924/
Go to the corresponding LIPIcs Volume Portal


Nigron, Pierre ; Dagand, Pierre-√Čvariste

Reaching for the Star: Tale of a Monad in Coq

pdf-format:
LIPIcs-ITP-2021-29.pdf (0.7 MB)


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}
}

Keywords: monads, hoare logic, separation logic, Coq
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: Software: https://github.com/Artalik/CompCert/tree/ITP archived at: https://archive.softwareheritage.org/swh:1:dir:bdd72cb914b59758fa869b3346e7674d1f8be2e4


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