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

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.

AUTOMATED COST ANALYSIS OF A PARALLEL MAXIMUM SEGMENT SUM PROGRAM DERIVATION

Static performance prediction of implicitly parallel functional programs can be facilitated by restricting the source language to be shapely [7]. The resulting analyses should provide valuable support for the calculational style of program derivation. We build upon previous work in the area by extending the range of admissible programs, allowing us to demonstrate the first automated analysis of a complete program derivation, that of the well known maximum segment sum algorithm of Skillicorn and Cai [11]. We examine the accuracy of our predictions against the run time of real parallel programs.