Hostname: page-component-8448b6f56d-m8qmq Total loading time: 0 Render date: 2024-04-19T06:22:27.866Z Has data issue: false hasContentIssue false
  • English
  • Français

Algebra of programming in Agda: Dependent types for relational program derivation

Part of: JFP Research Articles

Published online by Cambridge University Press:  23 July 2009

SHIN-CHENG MU ,
HSIANG-SHANG KO  and
PATRIK JANSSON
SHIN-CHENG MU
Affiliation:
Institute of Information Science, Academia Sinica, Taiwan (e-mail: scm@iis.sinica.edu.tw)
HSIANG-SHANG KO
Affiliation:
Department of Computer Science and Information Engineering, National Taiwan University, Taiwan (e-mail: joshs@mail2000.com.tw)
PATRIK JANSSON
Affiliation:
Department of Computer Science and Engineering, Chalmers University of Technology, and University of Gothenburg, Sweden (e-mail: patrikj@chalmers.se)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Relational program derivation is the technique of stepwise refining a relational specification to a program by algebraic rules. The program thus obtained is correct by construction. Meanwhile, dependent type theory is rich enough to express various correctness properties to be verified by the type checker. We have developed a library, AoPA (Algebra of Programming in Agda), to encode relational derivations in the dependently typed programming language Agda. A program is coupled with an algebraic derivation whose correctness is guaranteed by the type system. Two non-trivial examples are presented: an optimisation problem and a derivation of quicksort in which well-founded recursion is used to model terminating hylomorphisms in a language with inductive types.

Type
Articles
Information
Journal of Functional Programming , Volume 19 , Issue 5 , September 2009 , pp. 545 - 579
Copyright
Copyright © Cambridge University Press 2009

References

Agda Team, The. (2007) The Agda wiki [online]. Available at: http://wiki.portal.chalmers.se/agda/ (Accessed 3 July 2009).Google Scholar
Augustsson, L. (1998) Cayenne – a language with dependent types. In ACM SIGPLAN International Conference on Functional Programming, Felleisen, M., Hudak, P. & Queinnec, C. (eds), ACM Press, pp. 239–250.Google Scholar
Augustsson, L. (1999) Equality proofs in Cayenne [online]. Available at: http://www.cs.chalmers.se/~augustss/cayenne/eqproof.ps (Accessed 3 July 2009).Google Scholar
Backhouse, R. C. (2002) Galois connections and fixed point calculus. In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, Backhouse, R. C., Crole, R. & Gibbons, J. (eds), LNCS, no. 2297. Springer, pp. 89–148.CrossRefGoogle Scholar
Backhouse, R. C. & Hoogendijk, P. F. (1992) Elements of a relational theory of datatypes. In Formal Program Development, Möller, B., Partsch, H. A. & Schuman, S. A. (eds), LNCS, no. 755. Springer, pp. 7–42.Google Scholar
Backhouse, R. C., de Bruin, P. J., Malcolm, G., Voermans, E. & van der Woude, J. (1991) Relational catamorphisms. In IFIP TC2/WG2.1 Working Conference on Constructing Programs, Möller, B. (eds), Elsevier, pp. 287–318.Google Scholar
Bird, R. S. (1989a) Algebraic identities for program calculation, Comp. J., 32 (2): 122–126.CrossRefGoogle Scholar
Bird, R. S. (1989b) Lectures on constructive functional programming. In Constructive Methods in Computing Science, Broy, M. (ed), NATO ASI Series F, vol. 55. Springer, pp. 151–216.CrossRefGoogle Scholar
Bird, R. S. (1996) Functional algorithm design, Sci. Comp. Program., 26: 15–31.CrossRefGoogle Scholar
Bird, R. S. & de Moor, O. (1997) Algebra of Programming, International Series in Computer Science. Prentice Hall.Google Scholar
Bove, A. & Capretta, V. (2005) Modelling general recursion in type theory, Math. Struct. Comp. Sci., 15 (4): 671–708.CrossRefGoogle Scholar
Brady, E., McBride, C. & McKinna, J. (2003) Inductive families need not store their indices. In Types for Proofs and Programs, Berardi, S., Coppo, M. & Damiani, F. (eds), LNCS, vol. 3085. Springer, pp. 115–129.Google Scholar
Burstall, R. M. (1969) Proving properties of programs by structural induction, Comp. J., 12 (1): 41–48.CrossRefGoogle Scholar
Cheney, J. & Hinze, R. (2003) First-Class Phantom Types, Technical Report TR2003-1901. Cornell University.Google Scholar
Coq Development Team, The. (2006) The Coq Proof Assistant Reference Manual. LogiCal Project.Google Scholar
Cormen, T. H., Leiserson, C. E., Rivest, R. L. & Stein, C. (2001) Introduction to Algorithms. MIT Press.Google Scholar
Cousot, P. (1990) Method and logics for proving programs. In Formal Models and Semantics, van Leeuwen, J. (ed), Handbook of Theoretical Computer Science, vol. B. Elsevier, pp. 843–993.Google Scholar
Danielsson, N. A., Norell, U., Mu, S-C., Bronson, S., Doel, D., Jansson, P. & Chen, L-T. (2009) The Agda standard library [online]. Available at: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary (Accessed 3 July 2009).Google Scholar
Doornbos, H. (1996) Reductivity Arguments and Program Construction, PhD thesis. Eindhoven University of Technology.Google Scholar
Doornbos, H. & Backhouse, R. C. (1995) Induction and recursion on datatypes. In Mathematics of Program Construction 1995, LNCS, vol. 947. Springer, pp. 242–256.CrossRefGoogle Scholar
Doornbos, H. & Backhouse, R. C. (1996) Reductivity, Sci. Comp. Program., 26: 217–236.CrossRefGoogle Scholar
Dybjer, P. (1994) Inductive families, Formal Aspects Comput., 6 (4): 440–465.CrossRefGoogle Scholar
Dybjer, P. & Setzer, A. (1999) A finite axiomatization of inductive-recursive definitions. In TLCA'99, Girard, J.-Y. (ed), LNCS, vol. 1581. Springer, pp. 129–146.Google Scholar
Floyd, R. W. (1967) Assigning meanings to programs. In Mathematical Aspects of Computer Science, Schwartz, J. T. (ed), Proceedings of Symposia in Applied Mathematics, vol. 19. American Mathematical Society, pp. 19–32.CrossRefGoogle Scholar
Goguen, H., McBride, C. & McKinna, J. (2006) Eliminating dependent pattern matching. In Algebra, Meaning, and Computation, Futatsugi, K., Jouannaud, J.-P. & Meseguer, J. (eds), LNCS, vol. 4060. Springer, pp 521–540.CrossRefGoogle Scholar
Gonzalía, C. (2006) Relations in Dependent Type Theory, PhD thesis. Chalmers University of Technology.Google Scholar
Gries, D. (1989) The maximum-segment-sum problem. In Formal Development Programs and Proofs, Dijkstra, E. W. (ed), University of Texas at Austin Year of Programming Series. Addison-Wesley, pp. 33–36.Google Scholar
Harper, R. & Pollack, R. (1991) Type checking with universes, Theoret. Comp. Sci., 89 (1): 107–136.CrossRefGoogle Scholar
Leroy, X. (2006) Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In The 33th Symposium on Principles of Programming Languages. ACM Press, pp. 42–54.Google Scholar
Magnusson, L. & Nordström, B. (1994) The ALF proof editor and its proof engine. In Proceedings of the International Workshop on Types for Proofs and Programs. Springer, LNCS 806, pp. 213–237.CrossRefGoogle Scholar
McBride, C. & McKinna, J. (2004) The view from the left, J. Funct. Program., 14 (1): 69–111.CrossRefGoogle Scholar
McKinna, J. & Burstall, R. M. (1993) Deliverables: A categorical approach to program development in type theory. In International Symposium on Mathematical Foundations of Computer Science, Borzyszkowski, A. M. & Sokolowski, S. (eds), Springer, LNCS no. 711, pp. 32–67.Google Scholar
Megacz, A. (2007) A coinductive monad for prop-bounded recursion. In Proceedings of the ACM Workshop Programming Languages meets Program Verification, Stump, A. & Xi, H. (eds). ACM Press, pp. 11–20.Google Scholar
Meijer, E., Fokkinga, M. & Paterson, R. (1991) Functional programming with bananas, lenses, envelopes, and barbed wire. In ACM Conference on Functional Programming Languages and Computer Architecture, Hughes, J. (ed), Springer-Verlag, pp. 124–144.CrossRefGoogle Scholar
Mu, S-C. (2008) Maximum segment sum is back: deriving algorithms for two segment problems with bounded lengths. In ACM SIGPLAN 2008 Symposium on Partial Evaluation and Program Manipulation. ACM Press, pp. 31–39.CrossRefGoogle Scholar
Mu, S.-C. & Bird, R. S. (2003) Theory and applications of inverting functions as folds, Sci. Comp. Program., 51: 87–116.CrossRefGoogle Scholar
Mu, S-C., Ko, H-S. & Jansson, P. (2008a) Algebra of programming using dependent types. In Mathematics of Program Construction 2008, Audebaud, P. & Paulin-Mohring, C. (eds), Springer, LNCS 5133, pp. 268–283.CrossRefGoogle Scholar
Mu, S-C., Ko, H-S. & Jansson, P. (2008b) AoPA: Algebra of programming in Agda [online]. Available at: http://www.iis.sinica.edu.tw/~scm/2008/aopa/ (Accessed 3 July 2009).Google Scholar
Nordström, B. (1988) Terminating general recursion, BIT Numer. Math., 28 (3): 605–619.CrossRefGoogle Scholar
Norell, U. (2007) Towards a Practical Programming Language Based on Dependent Type Theory, PhD thesis. Chalmers University of Technology.Google Scholar
Paulin-Mohring, C. (1989) Extracting F ω's programs from proofs in the Calculus of Constructions. In Symposium on Principles of Programming Languages. ACM.Google Scholar
Sheard, T. & Linger, N. (2008) Central European Functional Programming School. In Programming in Ωmega, Horváth, Z., Plasmeijer, R., Soós, A. & Zsók, V. (eds), Springer-Verlag, LNCS no. 5161, pp. 158–227.Google Scholar
Sweeney, T. (2006) The next mainstream programming language: A game developer's perspective. In Symposium on Principles of Programming Languages, Charleston, SC, Jan. 11–13.Google Scholar
Tarski, A. (1955) A lattice-theoretic fixpoint theorem and its applications, Pacific. Math., 5: 285–309.CrossRefGoogle Scholar
Wadler, P. (1990) Deforestation: Transforming programs to eliminate trees, Theoret. Comp. Sci., 73: 231–248.CrossRefGoogle Scholar
Xi, H. (2007) Dependent ML: An approach to practical programming with dependent types, J. Funct. Program., 17 (2): 215–286.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.