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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
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_1
Bird, R., de Moor, O.: Algebra of Programming. Prentice-Hall Inc, Upper Saddle River (1997)
Capretta, V., Uustalu, T., Vene, V.: Recursive coalgebras from comonads. Inf. Comput. 204, 437–468 (2006)
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)
Chlipala, A.: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)
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_17
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)
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)
Loulergue, F., Bousdira, W., Tesson, J.: Calculating parallel programs in Coq using list homomorphisms. Int. J. Parallel Program. 45(2), 300–319 (2017)
Meertens, L.: Paramorphism. Formal Aspects Comput. 4(5), 413–424 (1992)
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_7
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)
Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, Cambridge (2011)
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)
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_10
The Coq development team: The Coq proof assistant reference manual (2018). https://coq.inria.fr/distrib/current/refman/. version 8.9.0
Uustalu, T., Vene, V.: Primitive (co)recursion and course-of-value (co)iteration, categorically. Informatica 10, 5–26 (1999)
Vene, V.: Categorical Programming with inductive and coinductive types. Ph.D. thesis, University of Tartu (2000)
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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Murata, K., Emoto, K. (2019). Recursion Schemes in Coq. In: Lin, A. (eds) Programming Languages and Systems. APLAS 2019. Lecture Notes in Computer Science(), vol 11893. Springer, Cham. https://doi.org/10.1007/978-3-030-34175-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-030-34175-6_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-34174-9
Online ISBN: 978-3-030-34175-6
eBook Packages: Computer ScienceComputer Science (R0)