K. Støvring and S. B. Lassen, “A Complete, Co-Inductive Syntactic Theory of Sequential Control and State”, BRICS, vol. 14, no. 4, Feb. 2007.