DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2021.29

Reaching for the Star: Tale of a Monad in Coq

Authors: Pierre Nigron and Pierre-Évariste Dagand

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

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.

Cite as

Pierre Nigron and Pierre-Évariste Dagand. Reaching for the Star: Tale of a Monad in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.ITP.2021.29},
  URN =		{urn:nbn:de:0030-drops-139241},
  doi =		{10.4230/LIPIcs.ITP.2021.29},
  annote =	{Keywords: monads, hoare logic, separation logic, Coq}
}

Search Results

Documents authored by Dagand, Pierre-Évariste

Reaching for the Star: Tale of a Monad in Coq

Abstract

Cite as

Thanks for your feedback!

Could not send message