  Realisability has been one of the first and principal tools in the research surrounding set theories based on intuitionistic logic, starting from the early contributions by Friedman and Myhill (Friedman 1973, Myhill 1973). Realisability semantics for intuitionistic arithmetic were first proposed by Kleene (Kleene 1945) and extended to higher order Heyting arithmetic by Kreisel and Troelstra (Kreisel and Troelstra 1970). For the definition of realisability for arithmetic see section 5.2 of the entry on intuitionistic logic. A realisability similar to Kreisel and Troelstra was applied to systems of higher order arithmetic by Friedman (Friedman 1973). Myhill introduced a variant of this realisability which resembles Kleene’s slash (Myhill 1973; Kleene 1962, 1963). He thus proved that a version of IZF with replacement in place of collection (called IZF\(_{Rep})\) has the DP, the NEP and the EP. These results were further extended in (Myhill 1975; Friedman and Scedrov 1983). While Friedman and Myhill gave realisability models for extensional set theories, Beeson developed a notion of realisability for non-extensional set theories. He then studied metatheoretical properties of the extensional set theories via an interpretation in their non-extensional counterparts. He thus proved that IZF (with collection) has the DP and NEP (Beeson 1985). Subsequently McCarty introduced realisability for IZF directly for extensional set theory (McCarty 1984; 1986). Realisability semantics for variants of CZF have been considered, for example, in (Crosilla and Rathjen 2001; Rathjen 2006a). The realisability in the latter article is inspired by McCarty’s and has the important feature that, as McCarty’s for IZF, it is a self-validating semantics for CZF (that is, this notion of realisability can be formalised in CZF and each theorem of CZF is realised provably in CZF). Rathjen has made use of this notion of realisability to show that CZF (and a number of extensions of it) have the DP and the NEP (Rathjen 2005b).