Algebra of programming using dependent types

author: Shin-Cheng Mu, Hsiang-Shang Ko and Patrik Jansson
publication date: 2008
cite this with: Shin-Cheng Mu, Hsiang-Shang Ko and Patrik Jansson. Algebra of programming using dependent types. In Mathematics of Program Construction. 2008.
link this with: http://tsm.iis.sinica.edu.tw/papers/mpc08/
copyright:
category: Functional programming, type theory
tag: program derivation, dependent type, Agda
full paper: PDF

Abstract

Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On the other hand, squiggolists know very well how to show that one relation is included in another by algebraic reasoning. We demonstrate how to encode functional and relational derivations in a dependently typed programming language. A program is coupled with an algebraic derivation from a specification, whose correctness is guaranteed by the type system.

Code accompanying the paper has been developed into an Agda library AoPA.

 
papers:mpc08:home Last modified: 2009/02/04 11:50