Document Open Access Logo

Extending Equational Monadic Reasoning with Monad Transformers

Authors Reynald Affeldt , David Nowak

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2020.2.pdf
  • Filesize: 0.87 MB
  • 21 pages

Document Identifiers

Author Details

Reynald Affeldt
  • National Institute of Advanced Industrial Science and Technology (AIST), Tokyo, Japan
David Nowak
  • Univ. Lille, CNRS, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France

Funding

We acknowledge the support of the JSPS KAKENHI Grant Number 18H03204.

Acknowledgements

We thank all the participants of the JSPS-CNRS bilateral program "FoRmal tools for IoT sEcurity" (PRC2199) for fruitful discussions. We also thank Takafumi Saikawa for his comments. This work is based on joint work with Célestine Sauvage [Célestine Sauvage et al., 2020].

Cite AsGet BibTex

Reynald Affeldt and David Nowak. Extending Equational Monadic Reasoning with Monad Transformers. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.TYPES.2020.2

Abstract

There is a recent interest for the verification of monadic programs using proof assistants. This line of research raises the question of the integration of monad transformers, a standard technique to combine monads. In this paper, we extend Monae, a Coq library for monadic equational reasoning, with monad transformers and we explain the benefits of this extension. Our starting point is the existing theory of modular monad transformers, which provides a uniform treatment of operations. Using this theory, we simplify the formalization of models in Monae and we propose an approach to support monadic equational reasoning in the presence of monad transformers. We also use Monae to revisit the lifting theorems of modular monad transformers by providing equational proofs and explaining how to patch a known bug using a non-standard use of Coq that combines impredicative polymorphism and parametricity.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Software and its engineering → Formal software verification
Keywords
  • monads
  • monad transformers
  • Coq
  • impredicativity
  • parametricity

Metrics

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

Related Versions

Supplementary Materials

References

  1. Reynald Affeldt, Jacques Garrigue, David Nowak, and Takafumi Saikawa. A trustful monad for axiomatic reasoning with probability and nondeterminism. arXiv cs.LO 2003.09993, 2020. URL: http://arxiv.org/abs/2003.09993.
  2. Reynald Affeldt, David Nowak, and Takafumi Saikawa. A hierarchy of monadic effects for program verification using equational reasoning. In 13th International Conference on Mathematics of Program Construction (MPC 2019), Porto, Portugal, October 7-9, 2019, volume 11825 of Lecture Notes in Computer Science, pages 226-254. Springer, 2019. Google Scholar
  3. Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Categorical structures for type theory in univalent foundations. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), August 20-24, 2017, Stockholm, Sweden, volume 82 of LIPIcs, pages 8:1-8:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. Google Scholar
  4. Robert Atkey, Neil Ghani, and Patricia Johann. A relationally parametric model of dependent type theory. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014), San Diego, CA, USA, January 20-21, 2014, pages 503-516. ACM, 2014. Google Scholar
  5. Jean-Philippe Bernardy and Guilhem Moulin. A computational interpretation of parametricity. In 27th Annual IEEE Symposium on Logic in Computer Science (LICS 2012), Dubrovnik, Croatia, June 25-28, 2012, pages 135-144. IEEE Computer Society, 2012. Google Scholar
  6. François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging mathematical structures. In 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), Munich, Germany, August 17-20, 2009, volume 5674 of Lecture Notes in Computer Science, pages 327-342. Springer, 2009. Google Scholar
  7. Herman Geuvers. Inconsistency of classical logic in type theory. Short note, December 2001. URL: http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz.
  8. Jeremy Gibbons. Unifying theories of programming with monads. In 4th International Symposium on Unifying Theories of Programming (UTP 2012), Paris, France, August 27-28, 2012, volume 7681 of Lecture Notes in Computer Science, pages 23-67. Springer, 2012. Google Scholar
  9. Jeremy Gibbons and Ralf Hinze. Just do it: simple monadic equational reasoning. In 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), Tokyo, Japan, September 19-21, 2011, pages 2-14. ACM, 2011. Google Scholar
  10. Georges Gonthier, Assia Mahboubi, and Enrico Tassi. A small scale reflection extension for the Coq system. Technical report, INRIA, 2008. Version 17 (Nov 2016). Now part of [The Coq Development Team, 2021]. Google Scholar
  11. Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for monadic types. Math. Struct. Comput. Sci., 18(6):1169-1217, 2008. Google Scholar
  12. Brian Huffman. Formal verification of monad transformers. In Peter Thiemann and Robby Bruce Findler, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012, pages 15-16. ACM, 2012. Google Scholar
  13. Infotheo. A Coq formalization of information theory and linear error-correcting codes. Coq scripts. Last stable release: 0.3, 2021. URL: https://github.com/affeldt-aist/infotheo/.
  14. Mauro Jaskelioff. Lifting of Operations in Modular Monadic Semantics. PhD thesis, University of Nottingham, 2009. Google Scholar
  15. Mauro Jaskelioff. Modular monad transformers. In 18th European Symposium on Programming (ESOP 2009), York, UK, March 22-29, 2009. Proceedings, volume 5502 of Lecture Notes in Computer Science, pages 64-79. Springer, 2009. Google Scholar
  16. Mauro Jaskelioff. Private communication, May 2020. Google Scholar
  17. Mauro Jaskelioff and Eugenio Moggi. Monad transformers as monoid transformers. Theor. Comput. Sci., 411(51-52):4441-4466, 2010. Google Scholar
  18. Chantal Keller and Marc Lasson. Parametricity in an impredicative sort. In 21st Annual Conference of the EACSL on Computer Science Logic (CSL 2012), September 3-6, 2012, Fontainebleau, France, volume 16 of LIPIcs, pages 381-395. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. Google Scholar
  19. Neelakantan R. Krishnaswami and Derek Dreyer. Internalizing relational parametricity in the extensional calculus of constructions. In Computer Science Logic 2013 (CSL 2013), September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 432-451. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. Google Scholar
  20. Sheng Liang, Paul Hudak, and Mark P. Jones. Monad transformers and modular interpreters. In 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1995), San Francisco, California, USA, January 23-25, 1995, pages 333-343. ACM Press, 1995. Google Scholar
  21. Kenji Maillard. Principes de la Vérification de Programmes à Effets Monadiques Arbitraires. PhD thesis, Université PSL, November 2019. Google Scholar
  22. Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, and Éric Tanter. Dijkstra monads for all. PACMPL, 3(ICFP):104:1-104:29, 2019. Google Scholar
  23. Mathematical Components Team. Mathematical Components library, 2007. Last stable version 1.11 (2020). URL: https://github.com/math-comp/math-comp.
  24. Monae. Monadic effects and equational reasoning in Coq. Coq scripts. Last stable release: 0.3, 2021. URL: https://github.com/affeldt-aist/monae/.
  25. Shin-Cheng Mu. Calculating a backtracking algorithm: An exercise in monadic program derivation. Technical Report TR-IIS-19-003, Institute of Information Science, Academia Sinica, June 2019. Google Scholar
  26. Shin-Cheng Mu. Equational reasoning for non-deterministic monad: A case study of Spark aggregation. Technical Report TR-IIS-19-002, Institute of Information Science, Academia Sinica, June 2019. Google Scholar
  27. Shin-Cheng Mu and Tsung-Ju Chiang. Declarative pearl: Deriving monadic quicksort. In Keisuke Nakano and Konstantinos Sagonas, editors, 15th International Symposium on Functional and Logic Programming (FLOPS 2020), Akita, Japan, September 14-16, 2020, volume 12073 of Lecture Notes in Computer Science, pages 124-138. Springer, 2020. Google Scholar
  28. Koen Pauwels, Tom Schrijvers, and Shin-Cheng Mu. Handling local state with global state. In 13th International Conference on Mathematics of Program Construction (MPC 2019), Porto, Portugal, October 7-9, 2019, volume 11825 of Lecture Notes in Computer Science, pages 18-44. Springer, 2019. Google Scholar
  29. Célestine Sauvage, Reynald Affeldt, and David Nowak. Vers la formalisation en Coq des transformateurs de monades modulaires. In Trente-et-unièmes Journées Francophones des Langages Applicatifs (JFLA 2020), Janvier 2020, Gruissan, France, pages 23-30, 2020. In French. URL: https://hal.archives-ouvertes.fr/hal-02434736v2/document.
  30. Tom Schrijvers, Maciej Piróg, Nicolas Wu, and Mauro Jaskelioff. Monad transformers and modular algebraic effects: what binds them together. In 12th ACM SIGPLAN International Symposium on Haskell (Haskell 2019), Berlin, Germany, August 18-23, 2019, pages 98-113. ACM, 2019. Google Scholar
  31. The Coq Development Team. Impredicative set, 2019. Last revision: 2019-07-12. URL: https://github.com/coq/coq/wiki/Impredicative-Set.
  32. The Coq Development Team. The Coq Proof Assistant Reference Manual. Inria, 2021. Version 8.13.0. URL: https://coq.inria.fr/distrib/current/refman/.
  33. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath - a computer-checked library of univalent mathematics. Available at URL: https://github.com/UniMath/UniMath.
  34. Philip Wadler. Theorems for free! In 4th international conference on Functional programming languages and computer architecture (FPCA 1989), London, UK, September 11-13, 1989, pages 347-359. ACM, 1989. Google Scholar
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 Imprint Privacy Contact