Reaching for the Star: Tale of a Monad in Coq - Sorbonne Université
Conference Papers Leibniz International Proceedings in Informatics Year : 2021

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.
Fichier principal
Vignette du fichier
LIPIcs-ITP-2021-29.pdf (738.89 Ko) Télécharger le fichier
Origin Publication funded by an institution

Dates and versions

hal-03266768 , version 1 (22-06-2021)

Identifiers

Cite

Pierre Nigron, Pierre-Évariste Dagand. Reaching for the Star: Tale of a Monad in Coq. 12th International Conference on Interactive Theorem Proving (ITP 2021), Jun 2021, Rome, Italy. pp.29:1--29:19, ⟨10.4230/LIPIcs.ITP.2021.29⟩. ⟨hal-03266768⟩
213 View
189 Download

Altmetric

Share

More