Laws of Programming
Isabelle/UTP contains a large library of algebraic laws of programming as theorems. We illustrate some of the relational laws below. The complete catalogue can be found in our Isabelle/UTP git repository, where you can find laws for predicate and relational calculus. Additional UTP theories, such as designs and reactive processes, further expand this to additional paradigms such as concurrency.
For browsing the Isabelle/UTP GitHub repository I recommend the very useful Matisa extension from my colleague Pedro Ribiero which typesets Isabelle using MathJax. It can be obtained for Google Chrome and also for Firefox.
Isabelle/UTP is supported by projects INTO-CPS, RoboCalc, and CyPhyAssure