In the calculational approach to programming, programs are derived from specifications by algebraic reasoning. This report presents a calculational programming framework based upon the notion of binary relations as programs, and partial equivalence relations (pers) as types. Working with relations as programs generalises the functional paradigm, admiting non-determinism and the use of relation converse. Working with pers as types permits a natural treatment of types that are subject to laws and restrictions.
Hutton, G., & Voermans, E. (1992). A Calculational Theory of Pers as Types. Department of Computing Science