 Another kind of realisability that has proved very useful is Lifschitz realisability. Lifschitz (1979) introduced a modification of Kleene’s realizability for Heyting arithmetic which has the peculiarity of validating a weak form of Church’s Thesis (CT) with a uniqueness condition, but not CT itself. Lifschitz realisability was extended to second order arithmetic by van Oosten (1990). It was subsequently extended to full IZF by Cheng and Rathjen, who employed it to obtain a number of independence results, as well as validating the so called Lesser Limited Principle of Omniscience (LLPO) (for LLPO see the entry on   constructive mathematics).