There are many variations on the theme of realizability model. Some such models tacitly assume set theory as the metatheory (Aczel 1980, Beeson 1985), whereas others explictly assume a constructive metatheory (Smith 1984).