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

8 weeks 2 days ago

8 weeks 4 days ago

8 weeks 6 days ago

15 weeks 5 days ago

21 weeks 3 days ago

21 weeks 4 days ago

22 weeks 3 days ago

25 weeks 2 days ago

26 weeks 5 days ago

26 weeks 5 days ago