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.

## Recent comments

5 days 10 hours ago

5 days 16 hours ago

6 days 9 hours ago

1 week 23 hours ago

1 week 6 days ago

2 weeks 14 hours ago

2 weeks 23 hours ago

2 weeks 1 day ago

2 weeks 5 days ago

3 weeks 1 day ago