Harel, D.; Kozen, D. A Programming Language for the Inductive Sets, and Applications. DPB 1982, 11.