Skip to main content
SpringerLink
Log in

Towards a Practical Library for Monadic Equational Reasoning in Coq

  • Conference paper
  • First Online:
Mathematics of Program Construction (MPC 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13544))

Included in the following conference series:

  • 368 Accesses

Abstract

Functional programs with side effects represented by monads are amenable to equational reasoning. This approach to program verification has been experimented several times using proof assistants based on dependent type theory. These experiments have been performed independently but reveal similar technicalities such as how to build a hierarchy of interfaces and how to deal with non-structural recursion. As an effort towards the construction of a reusable framework for monadic equational reasoning, we report on several practical improvements of Monae, a Coq library for monadic equational reasoning. First, we reimplement the hierarchy of effects of Monae using a generic tool to build hierarchies of mathematical structures. This refactoring allows for easy extensions with new monad constructs. Second, we discuss a well-known but recurring technical difficulty due to the shallow embedding of monadic programs. Concretely, it often happens that the return type of monadic functions is not informative enough to complete formal proofs, in particular termination proofs. We explain library support to facilitate this kind of proof using standard Coq tools. Third, we augment Monae with an improved theory about nondeterministic permutations so that our technical contributions allow for a complete formalization of quicksort derivations by Mu and Chiang.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 49.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 64.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Hierarchy-Builder version 1.1.0 (2021-03-30).

  2. 2.

    The existence of this intermediate interface is further justified by its use in the definition of the interface of the backtrackable state monad [14].

  3. 3.

    The command can be configured by the user so that Coq provides proofs automatically.

  4. 4.

    Since Coq already has a tactic, we call the function .

  5. 5.

    There is another axiom sorted-cat3, but its proof is easy using lemmas from MathComp.

  6. 6.

    The type Z_eqType is the type of integers equipped with decidable equality. This is a slight generalization of the original definition that is using natural numbers.

References

  1. Affeldt, R., Cohen, C., Kerjean, M., Mahboubi, A., Rouhling, D., Sakaguchi, K.: Competing inheritance paths in dependent type theory: a case study in functional analysis. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 3–20. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_1

    Chapter  Google Scholar 

  2. Affeldt, R., Garrigue, J., Nowak, D., Saikawa, T.: A trustful monad for axiomatic reasoning with probability and nondeterminism. J. Funct. Program. 31, e17 (2021). https://doi.org/10.1017/S0956796821000137

    Article  MathSciNet  MATH  Google Scholar 

  3. Affeldt, R., Nowak, D.: Extending equational monadic reasoning with monad transformers. In: 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics, vol. 188, pp. 2:1–2:21. Schloss Dagstuhl, June 2021. https://doi.org/10.4230/LIPIcs.TYPES.2020.2, https://arxiv.org/abs/2011.03463

  4. Affeldt, R., Nowak, D., Saikawa, T.: A hierarchy of monadic effects for program verification using equational reasoning. In: Hutton, G. (ed.) MPC 2019. LNCS, vol. 11825, pp. 226–254. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-33636-3_9

    Chapter  MATH  Google Scholar 

  5. Agda: Agda’s documentation v2.6.2.1 (2021). https://agda.readthedocs.io/en/v2.6.2.1/

  6. Barthe, G., Grégoire, B., Riba, C.: Type-based termination with sized products. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 493–507. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87531-4_35

    Chapter  Google Scholar 

  7. Benton, N., Hughes, J., Moggi, E.: Monads and effects. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 42–122. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45699-6_2

    Chapter  Google Scholar 

  8. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development–Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Cham (2004). https://doi.org/10.1007/978-3-662-07964-5

  9. Chan, J., Li, Y., Bowman, W.J.: Is sized typing for Coq practical? (2019). https://arxiv.org/abs/1912.05601

  10. Christiansen, J., Dylus, S., Bunkenburg, N.: Verifying effectful Haskell programs in Coq. In: 12th ACM SIGPLAN International Symposium on Haskell (Haskell 2019), Berlin, Germany, 18–23 August 2019, pp. 125–138. ACM (2019). https://doi.org/10.1145/3331545.3342592

  11. Cohen, C., Sakaguchi, K., Tassi, E.: Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi (system description). In: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), June 29-July 6, 2020, Paris, France (Virtual Conference). LIPIcs, vol. 167, pp. 34:1–34:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/LIPIcs.FSCD.2020.34

  12. Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327–342. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_23

    Chapter  Google Scholar 

  13. Garrigue, J.: Proving the correctness of OCaml typing by translation into Coq. In: The 17th Theorem Proving and Provers meeting (TPP 2021), November 2021. presentation

    Google Scholar 

  14. Gibbons, J., Hinze, R.: Just do it: simple monadic equational reasoning. In: 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), Tokyo, Japan, 19–21 September 2011. pp. 2–14. ACM (2011). https://doi.org/10.1145/2034773.2034777

  15. Hierarchy Builder: Hierarchy builder wiki–missingjoin. https://github.com/math-comp/hierarchy-builder/wiki/MissingJoin (2021)

  16. Jaskelioff, M.: Modular monad transformers. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 64–79. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00590-9_6

    Chapter  Google Scholar 

  17. Jomaa, N., Nowak, D., Grimaud, G., Hym, S.: Formal proof of dynamic memory isolation based on MMU. Sci. Comput. Program. 162, 76–92 (2018). https://doi.org/10.1016/j.scico.2017.06.012

    Article  Google Scholar 

  18. Letan, T., Régis-Gianas, Y.: FreeSpec: specifying, verifying, and executing impure computations in Coq. In: 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), New Orleans, LA, USA, 20–21 January 2020, pp. 32–46. ACM (2020). https://doi.org/10.1145/3372885.3373812

  19. Maillard, K., et al.: Dijkstra monads for all. Proc. ACM Program. Lang. 3(ICFP), 104:1–104:29 (2019). https://doi.org/10.1145/3341708

  20. MathComp: The mathematical components repository (2022). https://github.com/math-comp/math-comp. version 1.14.0. See sreflect/order.v for ordered types. See https://github.com/math-comp/math-comp/blob/251c8ec2490ff645a6afa45dd1ec238b9f71a554/mathcomp/ssreflect/tuple.v#L460-L499 for the bseq type

  21. Monae: Monadic effects and equational reasoning in Coq (2021). https://github.com/affeldt-aist/monae, version 0.4.1

  22. Mu, S.: Calculating a backtracking algorithm: an exercise in monadic program derivation. Technical report, Academia Sinica (2019). TR-IIS-19-003

    Google Scholar 

  23. Mu, S.: Equational reasoning for non-determinism monad: a case study of Spark aggregation. Technical report, Academia Sinica (2019). TR-IIS-19-002

    Google Scholar 

  24. Mu, S.-C., Chiang, T.-J.: Declarative pearl: deriving monadic quicksort. In: Nakano, K., Sagonas, K. (eds.) FLOPS 2020. LNCS, vol. 12073, pp. 124–138. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-59025-3_8

    Chapter  Google Scholar 

  25. Oliveira, B.C.D.S., Schrijvers, T., Cook, W.R.: MRI: Modular reasoning about interference in incremental programming. J. Funct. Program. 22, 797–852 (2012). https://doi.org/10.1017/S0956796812000354

    Article  MathSciNet  MATH  Google Scholar 

  26. Pauwels, K., Schrijvers, T., Mu, S.-C.: Handling local state with global state. In: Hutton, G. (ed.) MPC 2019. LNCS, vol. 11825, pp. 18–44. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-33636-3_2

    Chapter  Google Scholar 

  27. Sakaguchi, K.: Program extraction for mutable arrays. Sci. Comput. Program. 191, 102372 (2020). https://doi.org/10.1016/j.scico.2019.102372

    Article  Google Scholar 

  28. Schrijvers, T., Piróg, M., Wu, N., Jaskelioff, M.: Monad transformers and modular algebraic effects: what binds them together. In: 12th ACM SIGPLAN International Symposium on Haskell (Haskell 2019), Berlin, Germany, 18–23 August 2019, pp. 98–113. ACM (2019). https://doi.org/10.1145/3331545.3342595

  29. Sozeau, M.: Equations–a function definitions plugin (2009). https://mattam82.github.io/Coq-Equations/. last stable release: 1.3 (2021)

  30. Sozeau, M., Mangin, C.: Equations reloaded: high-level dependently-typed functional programming and proving in coq. Proc. ACM Program. Lang. 3(ICFP), 86:1-86:29 (2019). https://doi.org/10.1145/3341690

    Article  Google Scholar 

  31. The Coq Development Team: The Coq Proof Assistant Reference Manual. Inria (2022). https://coq.inria.fr. Version 8.15.1

Download references

Acknowledgements

The authors would like to thank Cyril Cohen and Enrico Tassi for their assistance with Hierarchy-Builder, Kazuhiko Sakaguchi and Takafumi Saikawa for their comments, the members of the Programming Research Group of the Department of Mathematical and Computing Science at the Tokyo Institute of Technology for their input, and the anonymous reviewers for many comments that improved this paper. The second author acknowledges the support of the JSPS KAKENHI grants 18H03204 and 22H00520.

Author information

Authors and Affiliations

  1. Tokyo Institute of Technology, School of Computing, Department of Mathematical and Computing Science, Tokyo, Japan

    Ayumu Saito

  2. National Institute of Advanced Industrial Science and Technology (AIST), Tokyo, Japan

    Reynald Affeldt

Authors
  1. Ayumu Saito
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Reynald Affeldt
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Reynald Affeldt .

Editor information

Editors and Affiliations

  1. School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh, UK

    Ekaterina Komendantskaya

Rights and permissions

Reprints and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Saito, A., Affeldt, R. (2022). Towards a Practical Library for Monadic Equational Reasoning in Coq. In: Komendantskaya, E. (eds) Mathematics of Program Construction. MPC 2022. Lecture Notes in Computer Science, vol 13544. Springer, Cham. https://doi.org/10.1007/978-3-031-16912-0_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-16912-0_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-16911-3

  • Online ISBN: 978-3-031-16912-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation