Generalizing the higher-order frame and anti-frame rules
François Pottier · 2009
This informal note presents generalized versions of the higherorder frame and anti-frame rules. The main insights reside in two successive generalizations of the “tensor” operator ›. In the first step, a form of “local invariant”, which allows implicit reasoning about “well-bracketed state changes”, is introduced. In the second step, a form of “local monotonicity” is added.