Advertisement

Recursion Schemes in Coq

  • Kosuke MurataEmail author
  • Kento Emoto
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11893)

Abstract

Program calculation, a programming technique to derive efficient programs from naive ones by program transformation, is challenging for program optimization. Tesson et al. have shown that Coq, a popular proof assistant, provides a cost-effective way to implement a powerful system for verifying correctness of program transformations, but their applications are limited to list functions in the Theory of Lists. In this paper, we propose an easy-to-use Coq library to prove more advanced calculation rules in Coq for various recursion schemes, which capture recursive programs on an arbitrary algebraic datatype. We prove all the lemmas and theorems about recursion schemes in Coq including histomorphisms and futumorphisms proposed by Uustalu et al. Our library can be used to obtain certified runnable programs from their definitions written with recursion schemes in Coq scripts. We demonstrate a certified runnable program for the Fibonacci numbers and unbounded knapsack problem from their histomorphic definitions.

Keywords

Program calculation Functional programming Recursion schemes Coq 

Notes

Acknowledgements

We thank Jeremy Gibbons for his great shepherding of this paper. We are also grateful to the anonymous reviewers for their valuable feedback. This work was supported by JSPS KAKENHI Grant Number JP19K11903.

References

  1. 1.
    Bird, R.S.: An introduction to the theory of lists. In: Broy, M. (ed.) Logic of Programming and Calculi of Discrete Design. NATO ASI Series (Series F: Computer and Systems Sciences), vol. 36, pp. 5–42. Springer, Heidelberg (1987).  https://doi.org/10.1007/978-3-642-87374-4_1CrossRefGoogle Scholar
  2. 2.
    Bird, R., de Moor, O.: Algebra of Programming. Prentice-Hall Inc, Upper Saddle River (1997)zbMATHGoogle Scholar
  3. 3.
    Capretta, V., Uustalu, T., Vene, V.: Recursive coalgebras from comonads. Inf. Comput. 204, 437–468 (2006)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Chiang, Y.H., Mu, S.C.: Formal derivation of greedy algorithms from relational specifications: a tutorial. J. Logical Algebraic Methods Program. 85, 879–905 (2016)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Chlipala, A.: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)CrossRefGoogle Scholar
  6. 6.
    Emoto, K., Loulergue, F., Tesson, J.: A verified generate-test-aggregate Coq library for parallel programs extraction. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 258–274. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08970-6_17CrossRefGoogle Scholar
  7. 7.
    Hinze, R., Wu, N., Gibbons, J.: Unifying structured recursion schemes. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming ICFP 2013, pp. 209–220. ACM, New York (2013)Google Scholar
  8. 8.
    Hu, Z., Iwasaki, H., Takeichi, M.: Deriving structural hylomorphisms from recursive definitions. In: Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, ICFP 1996, pp. 73–82 (1996)Google Scholar
  9. 9.
    Loulergue, F., Bousdira, W., Tesson, J.: Calculating parallel programs in Coq using list homomorphisms. Int. J. Parallel Program. 45(2), 300–319 (2017)CrossRefGoogle Scholar
  10. 10.
    Meertens, L.: Paramorphism. Formal Aspects Comput. 4(5), 413–424 (1992)CrossRefGoogle Scholar
  11. 11.
    Meijer, E., Fokkinga, M., Paterson, R.: Functional programming with bananas, lenses, envelopes and barbed wire. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol. 523, pp. 124–144. Springer, Heidelberg (1991).  https://doi.org/10.1007/3540543961_7CrossRefGoogle Scholar
  12. 12.
    Mu, S.C., Ko, H.S., Jansson, P.: Algebra of programming in Agda: dependent types for relational program derivation. J. Funct. Program. 19(5), 545–579 (2009)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, Cambridge (2011)Google Scholar
  14. 14.
    Takano, A., Meijer, E.: Shortcut deforestation in calculational form. In: Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture FPCA 1995, pp. 306–313. ACM, New York (1995)Google Scholar
  15. 15.
    Tesson, J., Hashimoto, H., Hu, Z., Loulergue, F., Takeichi, M.: Program calculation in Coq. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 163–179. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-17796-5_10CrossRefGoogle Scholar
  16. 16.
    The Coq development team: The Coq proof assistant reference manual (2018). https://coq.inria.fr/distrib/current/refman/. version 8.9.0
  17. 17.
    Uustalu, T., Vene, V.: Primitive (co)recursion and course-of-value (co)iteration, categorically. Informatica 10, 5–26 (1999)MathSciNetzbMATHGoogle Scholar
  18. 18.
    Vene, V.: Categorical Programming with inductive and coinductive types. Ph.D. thesis, University of Tartu (2000)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Kyushu Institute of TechnologyKitakyushuJapan

Personalised recommendations