Recursion Schemes in Coq
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.
KeywordsProgram calculation Functional programming Recursion schemes Coq
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.
- 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.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
- 13.Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, Cambridge (2011)Google Scholar
- 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
- 16.The Coq development team: The Coq proof assistant reference manual (2018). https://coq.inria.fr/distrib/current/refman/. version 8.9.0
- 18.Vene, V.: Categorical Programming with inductive and coinductive types. Ph.D. thesis, University of Tartu (2000)Google Scholar