  Intuitionistic versions of Zermelo-Fraenkel set theories were introduced in the early 1970s by Friedman and Myhill. In (Friedman 1973) the author presents a study of formal properties of various intuitionistic systems and introduces for them an extension of Kleene’s realisability method. The realisability technique is applied in (Myhill 1973) to show the existence property for a version of intuitionistic Zermelo-Fraenkel set theory (with replacement in place of collection). In another fundamental contribution Friedman extends the double negation translation of intuitonistic logic to relate classical and intuitionistic set theories (Friedman 1973a). These first papers already address the relation between some major intuitionistic set theories and classical ZF. They also clarify a key feature of set theory based on intuitionistic logic, mainly that it is amenable to powerful constructive semantic interpretations, like realizability. These techniques are applied to the study of crucial metatheoretical properties which are typical of the constructive approach and which are enjoyed by some constructive set theories (see the section on  Semantic techniques).  This groundbreaking work has been fully exploited and substantially extended in work by Beeson and McCarty (see Beeson 1985; McCarty 1984).