Generalizing realizability and Heyting models for constructive set theory

This article presents a common generalization of the two main methods for obtaining class models of constructive set theory. Heyting models are a generalization of the Boolean models for classical set theory which are a variant of forcing, while realizability is a decidedly constructive method that has first been developed for number theory by Kleene and was later very fruitfully adapted to constructive set theory. In order to achieve the...