A Calculational Theory of Pers as Types - Hutton, Graham; Voermans, Ed (Department of Computing Science, 1992)
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.