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

author: Shin-Cheng Mu, Hsiang-Shang Ko and Patrik Jansson
publication date: 2009
cite this with: Shin-Cheng Mu, Hsiang-Shang Ko and Patrik Jansson. Algebra of programming in Agda: dependent types for relational program derivation. To appear in Journal of Functional Programming. 2009.
link this with: http://tsm.iis.sinica.edu.tw/papers/jfp09/
copyright: All rights reserved
category: functional programming, type theory
tag: program derivation, dependent type, Agda
full paper: PDF

Abstract

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, 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 where well-founded recursion is used to model terminating hylomorphisms in a language with inductive types.

This article extends the paper we published in Mathematics of Program Construction 2008. Code accompanying the paper has been developed into an Agda library AoPA.

 
papers:jfp09:home Last modified: 2009/02/04 11:55