We present a general axiomatic construction of models of FPC,
a recursively typed lambda-calculus with call-by-value
operational semantics. Our method of construction is to obtain
such models as full subcategories of categorical
models of intuitionistic set theory. We show that
the existence of solutions to recursive domain equations,
needed for the interpretation of recursive
types, depends on the strength of the set theory.
The internal set theory of an elementary topos is not
strong enough to guarantee their existence.
However, using models of intuitionistic Zermelo-Fraenkel
set theory instead, we prove an algebraic compactness result.
We apply this to obtain an interpretation of FPC in any model.
Lastly, we provide necessary and sufficient conditions on a model
for the interpretation to be computationally adequate, i.e. for
the operational and denotational notions of convergence to
agree.
