Document Open Access Logo

Reaching for the Star: Tale of a Monad in Coq

Authors Pierre Nigron, Pierre-Évariste Dagand

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.29.pdf
  • Filesize: 0.72 MB
  • 19 pages

Document Identifiers

Author Details

Pierre Nigron
  • Sorbonne Université, CNRS, Inria, LIP6, Paris, France
Pierre-Évariste Dagand
  • Sorbonne Université, CNRS, Inria, LIP6, Paris, France

Funding

  • Nigron, Pierre: "Ministère des armées - Agence de l'Innovation de Défense" grant.
  • Dagand, Pierre-Évariste: Emergence(s) - Ville de Paris grant.

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.ITP.2021.29

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software notations and tools
Keywords
  • monads
  • hoare logic
  • separation logic
  • Coq

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Reynald Affeldt, David Nowak, and Takafumi Saikawa. A hierarchy of monadic effects for program verification using equational reasoning. In Graham Hutton, editor, Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings, volume 11825 of Lecture Notes in Computer Science, pages 226-254. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-33636-3_9.
  2. Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy. Recalling a witness: foundations and applications of monotonic state. Proc. ACM Program. Lang., 2(POPL):65:1-65:30, 2018. URL: https://doi.org/10.1145/3158153.
  3. Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. Dijkstra monads for free. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 515-529. ACM, 2017. URL: https://doi.org/10.1145/3093333.3009878.
  4. Robert Atkey. Parameterised notions of computation. J. Funct. Program., 19(3-4):335-376, 2009. URL: https://doi.org/10.1017/S095679680900728X.
  5. Nick Benton, Chung-Kil Hur, Andrew Kennedy, and Conor McBride. Strongly typed term representations in coq. J. Autom. Reason., 49(2):141-159, 2012. URL: https://doi.org/10.1007/s10817-011-9219-0.
  6. Edwin Brady. Programming and reasoning with algebraic effects and dependent types. In ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 133-144, 2013. URL: https://doi.org/10.1145/2500365.2500581.
  7. Edwin Brady. Resource-dependent algebraic effects. In Trends in Functional Programming - 15th International Symposium, TFP 2014, Soesterberg, The Netherlands, May 26-28, 2014. Revised Selected Papers, pages 18-33, 2014. URL: https://doi.org/10.1007/978-3-319-14675-1_2.
  8. Arthur Charguéraud. Program verification through characteristic formulae. In Paul Hudak and Stephanie Weirich, editors, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 321-332. ACM, 2010. URL: https://doi.org/10.1145/1863543.1863590.
  9. Arthur Charguéraud. Separation logic for sequential programs (functional pearl). Proc. ACM Program. Lang., 4(ICFP):116:1-116:34, 2020. URL: https://doi.org/10.1145/3408998.
  10. Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, and Katherine Ye. The end of history? using a proof assistant to replace language design with library design. In Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi, editors, 2nd Summit on Advances in Programming Languages, SNAPL 2017, May 7-10, 2017, Asilomar, CA, USA, volume 71 of LIPIcs, pages 3:1-3:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.SNAPL.2017.3.
  11. Jean-Christophe Filliâtre. Verification of non-functional programs using interpretations in type theory. J. Funct. Program., 13(4):709-745, 2003. URL: https://doi.org/10.1017/S095679680200446X.
  12. Jeremy Gibbons and Ralf Hinze. Just do it: simple monadic equational reasoning. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 2-14, 2011. URL: https://doi.org/10.1145/2034773.2034777.
  13. Michael Hicks, Gavin M. Bierman, Nataliya Guts, Daan Leijen, and Nikhil Swamy. Polymonadic programming. In Paul Levy and Neel Krishnaswami, editors, Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2014, Grenoble, France, 12 April 2014, volume 153 of EPTCS, pages 79-99, 2014. URL: https://doi.org/10.4204/EPTCS.153.7.
  14. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576-580, 1969. URL: https://doi.org/10.1145/363235.363259.
  15. Graham Hutton and Diana Fulger. Reasoning About Effects: Seeing the Wood Through the Trees. In Proceedings of the Symposium on Trends in Functional Programming, Nijmegen, The Netherlands, May 2008. Google Scholar
  16. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28:e20, 2018. URL: https://doi.org/10.1017/S0956796818000151.
  17. Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. Mosel: a general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang., 2(ICFP):77:1-77:30, 2018. URL: https://doi.org/10.1145/3236772.
  18. Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, 2009. URL: https://doi.org/10.1145/1538788.1538814.
  19. Thomas Letan and Yann Régis-Gianas. Freespec: specifying, verifying, and executing impure computations in Coq. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 32-46. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373812.
  20. Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, and Guillaume Hiet. Modular verification of programs with effects and effect handlers in Coq. In Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings, pages 338-354, 2018. URL: https://doi.org/10.1007/978-3-319-95582-7_20.
  21. Kenji Maillard. Principles of Program Verification for Arbitrary Monadic Effects. (Principes de la Vérification de Programmes à Effets Monadiques Arbitraires). PhD thesis, École Normale Supérieure, Paris, France, 2019. URL: https://tel.archives-ouvertes.fr/tel-02416788.
  22. Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, and Éric Tanter. Dijkstra monads for all. Proc. ACM Program. Lang., 3(ICFP):104:1-104:29, 2019. URL: https://doi.org/10.1145/3341708.
  23. Iris development team. coq-std++. URL: https://plv.mpi-sws.org/coqdoc/stdpp.
  24. Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: dependent types for imperative programs. In James Hook and Peter Thiemann, editors, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, pages 229-240. ACM, 2008. URL: https://doi.org/10.1145/1411204.1411237.
  25. Aleksandar Nanevski, J. Gregory Morrisett, and Lars Birkedal. Hoare type theory, polymorphism and separation. J. Funct. Program., 18(5-6):865-911, 2008. URL: https://doi.org/10.1017/S0956796808006953.
  26. Simon Peyton Jones. Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell, pages 47-96. IOS Press, January 2001. Google Scholar
  27. Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cǎtǎlin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. Programming Language Foundations. Software Foundations series, volume 2. Electronic textbook, 2018. Google Scholar
  28. Gordon D. Plotkin and John Power. Adequacy for algebraic effects. In Furio Honsell and Marino Miculan, editors, Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, volume 2030 of Lecture Notes in Computer Science, pages 1-24. Springer, 2001. URL: https://doi.org/10.1007/3-540-45315-6_1.
  29. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 55-74. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  30. Christoph Sprenger and David A. Basin. A monad-based modeling and verification toolbox with application to security protocols. In Klaus Schneider and Jens Brandt, editors, Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, volume 4732 of Lecture Notes in Computer Science, pages 302-318. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74591-4_23.
  31. Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin. Dependent types and multi-monadic effects in F. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 256-270. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837655.
  32. Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, and Guido Martínez. Steelcore: an extensible concurrent separation logic for effectful dependently typed programs. Proc. ACM Program. Lang., 4(ICFP):121:1-121:30, 2020. URL: https://doi.org/10.1145/3409003.
  33. Wouter Swierstra. A hoare logic for the state monad. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 440-451. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_30.
  34. Wouter Swierstra. The hoare state monad (proof pearl), 2009. Google Scholar
  35. Wouter Swierstra and Tim Baanen. A predicate transformer semantics for effects (functional pearl). Proc. ACM Program. Lang., 3(ICFP):103:1-103:26, 2019. URL: https://doi.org/10.1145/3341707.
  36. Iain Whiteside, David Aspinall, and Gudmund Grov. An essence of ssreflect. In Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, and Volker Sorge, editors, Intelligent Computer Mathematics - 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings, volume 7362 of Lecture Notes in Computer Science, pages 186-201. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31374-5_13.
  37. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang., 4(POPL):51:1-51:32, 2020. URL: https://doi.org/10.1145/3371119.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact