×

zbMATH — the first resource for mathematics

Algebra of programming in Agda: dependent types for relational program derivation. (English) Zbl 1191.68195
Summary: 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.

MSC:
68N99 Theory of software
68Q65 Abstract data types; algebraic specification
Software:
Coq; AoPA; Agda; Cayenne; ALF
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] DOI: 10.1093/comjnl/32.2.122
[2] Bird, Constructive Methods in Computing Science pp 151– (1989)
[3] Backhouse, IFIP TC2/WG2.1 Working Conference on Constructing Programs pp 287– (1991)
[4] DOI: 10.1145/1328408.1328414
[5] Backhouse, Formal Program Development pp 7– (1992)
[6] Meijer, ACM Conference on Functional Programming Languages and Computer Architecture pp 124– (1991)
[7] DOI: 10.1007/3-540-47797-7_4
[8] DOI: 10.1145/1292597.1292601
[9] McKinna, International Symposium on Mathematical Foundations of Computer Science pp 32– (1993)
[10] DOI: 10.1145/289423.289451 · Zbl 1369.68085
[11] DOI: 10.1017/S0956796803004829 · Zbl 1069.68539
[12] Magnusson, Proceedings of the International Workshop on Types for Proofs and Programs pp 213– (1994)
[13] Leroy, The 33th Symposium on Principles of Programming Languages pp 42– (2006)
[14] DOI: 10.1016/0304-3975(90)90108-T · Zbl 0737.68013
[15] Gries, Formal Development Programs and Proofs pp 33– (1989)
[16] DOI: 10.1007/11780274_27 · Zbl 1132.68327
[17] Floyd, Mathematical Aspects of Computer Science pp 19– (1967)
[18] Dybjer, TLCA’99 pp 129– (1999)
[19] DOI: 10.1007/BF01211308 · Zbl 0808.03044
[20] DOI: 10.1016/0167-6423(95)00027-5 · Zbl 0848.68054
[21] Doornbos, Mathematics of Program Construction 1995 pp 242– (1995)
[22] Cousot, Formal Models and Semantics pp 843– (1990)
[23] Cormen, Introduction to Algorithms (2001)
[24] The Coq Proof Assistant Reference Manual (2006)
[25] DOI: 10.1017/S0956796806006216 · Zbl 1125.68033
[26] Cheney, First-Class Phantom Types (2003)
[27] DOI: 10.1016/0304-3975(90)90147-A · Zbl 0701.68013
[28] Burstall, Comp. J. 12 pp 41– (1969) · Zbl 0164.46202
[29] Tarski, Pacific. Math. 5 pp 285– (1955) · Zbl 0064.26004
[30] Brady, Types for Proofs and Programs pp 115– (2003)
[31] Sweeney, Symposium on Principles of Programming Languages (2006)
[32] DOI: 10.1017/S0960129505004822 · Zbl 1084.03026
[33] Bird, Algebra of Programming (1997)
[34] Sheard, Programming in {\(\Omega\)}mega pp 158– (2008)
[35] Paulin-Mohring, Symposium on Principles of Programming Languages (1989)
[36] DOI: 10.1007/BF01941137 · Zbl 0659.68020
[37] DOI: 10.1016/0167-6423(95)00033-X · Zbl 0853.68101
[38] DOI: 10.1007/978-3-540-70594-9_15 · Zbl 1156.68358
[39] DOI: 10.1016/j.scico.2003.09.003 · Zbl 1091.68026
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.