Relational systems allow efficient comparison of two programs. Provided a relationship between the inputs of the programs, one can derive a relationship between the outputs. A wide range of security, privacy, and robustness properties become tractable with such an approach. Examples include non-interference, differential privacy, expected sensitivity, and cost analysis.

While several implementations of relational type and proof systems are actively developing, none of them have achieved full practical appeal yet. In this extended abstract, I present a library safe-coupling that enables relational reasoning about Haskell programs. This work gives the first implementation to a proof method described in a line of work on Relational Higher-Order Logic (RHOL). In particular, the core of safe-coupling comprises mechanisms to reason about non-deterministic higher-order programs inspired by probabilistic extensions of RHOL.

The library uses a refinement type system of Liquid Haskell to implement relations at the type level as boolean predicates. This allows enough flexibility to approach the expressiveness of RHOL while also providing SMT-powered automation for arithmetic. Thus, a new balance of generality and practicality is attained for the relational verification of higher-order programs.