IZF is a well investigated impredicative constructive version of
Zermelo-Fraenkel set theory. Using set terms, we axiomatize IZF with
Replacement, which we call IZF_R , along with its intensional
counterpart IZF_R^- . We define a typed lambda
calculus λZ corresponding to proofs in
IZF_R^- according to the Curry-Howard isomorphism
principle. Using realizability for IZF_R^- , we show
weak normalization of λZ . We use normalization to prove the
disjunction, numerical existence and term existence properties. An inner
extensional model is used to show these properties, along with the set
existence property, for full, extensional IZF_R .