Algebra of programming using dependent types

Algebra of programming using dependent types. S-C. Mu, H-S. Ko, and P. Jansson.

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.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


How is Agda an improvement over Coq for this kind of programming?


Coq does not really support a refinement mode where you write the proof terms incrementally. Instead it has a tactic system, where you don't see the lambda term being built and work at a higher level of abstraction. It seems to me the development could be done using generalized rewriting tactics as available in Coq (and other assistants like NuPRL) but I have no proof yet :)