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

16 hours 49 min ago

2 days 17 hours ago

3 days 17 hours ago

4 days 11 hours ago

4 days 20 hours ago

6 days 16 hours ago

6 days 21 hours ago

1 week 8 hours ago

1 week 8 hours ago

1 week 3 days ago