Abstract
Program calculation, being a programming technique that derives programs from specification by means of formula manipulation, is a challenging activity. It requires human insights and creativity, and needs systems to help human to focus on clever parts of the derivation by automating tedious ones and verifying correctness of transformations. Different from many existing systems, we show in this paper that Coq, a popular theorem prover, provides a cheap way to implement a powerful system to support program calculation, which has not been recognized so far. We design and implement a set of tactics for the Coq proof assistant to help the user to derive programs by program calculation and to write proofs in calculational form. The use of these tactics is demonstrated through program calculations in Coq based on the theory of lists.
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
Preview
Unable to display preview. Download preview PDF.
References
Bird, R.: Constructive functional programming. In: STOP Summer School on Constructive Algorithmics, Abeland (September 1989)
Kaldewaij, A.: Programming: the derivation of algorithms. Prentice-Hall, Inc., Upper Saddle River (1990)
Bird, R., de Moor, O.: Algebra of Programming. Prentice-Hall, Englewood Cliffs (1996)
Bird, R.: An introduction to the theory of lists. In: Broy, M. (ed.) Logic of Programming and Calculi of Discrete Design, pp. 5–42. Springer, Heidelberg (1987)
Gibbons, J.: Algebras for Tree Algorithms. D. phil thesis (1991); Also available as Technical Monograph PRG-94
de Moor, O.: Categories, relations and dynamic programming. Ph.D thesis, Programming research group, Oxford Univ. (1992) Technical Monograph PRG-98
Hu, Z., Takeichi, M., Chin, W.N.: Parallelization in calculational forms. In: POPL 1998: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 316–328. ACM Press, New York (1998)
Smith, D.R.: KIDS — a knowledge-based software development system. In: Lowry, M.R., Mccartney, R.D. (eds.) Automating Software Design, Menlo Park, CA, pp. 483–514. AAAI Press / The MIT Press (1991)
de Moor, O., Sittampalam, G.: Generic program transformation. In: Swierstra, S.D., Oliveira, J.N. (eds.) AFP 1998. LNCS, vol. 1608. Springer, Heidelberg (1999)
Yokoyama, T., Hu, Z., Takeichi, M.: Yicho: A system for programming program calculations. Technical Report METR 2002–07, Department of Mathematical Engineering, University of Tokyo (June 2002)
Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development – Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)
Sozeau, M., Oury, N.: First-Class Type Classes. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278–293. Springer, Heidelberg (2008)
Visser, E.: A survey of strategies in rule-based program transformation systems. J. Symb. Comput. 40(1), 831–873 (2005)
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)
Augustsson, L.: Cayenne - a language with dependent types. In: In International Conference on Functional Programming, pp. 239–250. ACM Press, New York (1998)
McBride, C.: Epigram: Practical programming with dependent types. In: Vene, V., Uustalu, T. (eds.) AFP 2004. LNCS, vol. 3622, pp. 130–170. Springer, Heidelberg (2005)
Norell, U.: Dependently typed programming in agda. In: Kennedy, A., Ahmed, A. (eds.) TLDI, pp. 1–2. ACM, New York (2009)
Corbineau, P.: A Declarative Language for the Coq Proof Assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941, pp. 69–84. Springer, Heidelberg (2008)
Meertens, L.: Calculate Polytypically! In: Kuchen, H., Swierstra, S.D. (eds.) PLILP 1996. LNCS, vol. 1140, pp. 1–16. Springer, Heidelberg (1996)
Verbruggen, W., de Vries, E., Hughes, A.: Polytypic programming in Coq. In: WGP 2008: Proceedings of the ACM SIGPLAN Workshop on Generic Programming, pp. 49–60. ACM Press, New York (2008)
Verbruggen, W., de Vries, E., Hughes, A.: Polytypic properties and proofs in Coq. In: WGP 2009: Proceedings of the 2009 ACM SIGPLAN Workshop on Generic Programming, pp. 1–12. ACM Press, New York (2009)
The Coq Development Team: The Coq Proof Assistant, http://coq.inria.fr
Bertot, Y.: Coq in a hurry (2006), http://hal.inria.fr/inria-00001173
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tesson, J., Hashimoto, H., Hu, Z., Loulergue, F., Takeichi, M. (2011). Program Calculation in Coq. In: Johnson, M., Pavlovic, D. (eds) Algebraic Methodology and Software Technology. AMAST 2010. Lecture Notes in Computer Science, vol 6486. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17796-5_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-17796-5_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17795-8
Online ISBN: 978-3-642-17796-5
eBook Packages: Computer ScienceComputer Science (R0)