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

6 days 11 hours ago

6 days 14 hours ago

6 days 15 hours ago

1 week 2 days ago

1 week 3 days ago

1 week 4 days ago

1 week 4 days ago

1 week 5 days ago

1 week 5 days ago

1 week 5 days ago