We investigate the relation between the semantic models of Z, as proposed by the Z draft standard, and of the polymorphic version of higher-order logic that is the basis for proof systems such as HOL and Isabelle/HOL. Disregarding the names in schema types, the type models of the two systems can be identified up to isomorphism. That isomorphism determines to a large extent how terms of Z can be represented in higher-order logic. This justifies the soundness of proof support for Z based on higher-order logic, such as the encoding of Z in Isabelle/HOL.
The comparison of the two semantic models also motivates a discussion of open issues in the development of a complete semantics of Z, in particular concerning the type system, generic constructs, and approaches to base the semantics of Z on a small kernel language.