D. Harel and D. Kozen, “A Programming Language for the Inductive Sets, and Applications”, DPB, vol. 11, no. 143, Apr. 1982.