   Heyting-valued semantics for intuitionistic set theories were obtained by Grayson (Grayson 1979) as a counterpart for Boolean models for classical set theory. They have been generalized especially via categorical semantics (for an introduction see MacLane and Moerdijk 1992).  Heyting-valued semantics  have found application to independence results in (Scedrov 1981; 1982). A constructive treatment has been given in (Gambino 2006). See also (Lubarsky 2009).  See also Ziegler (2012) for a generalization of realisability and Heyting models for constructive set theory. 