We define (set-theoretic) notions of intensional Henkin model and syntactic lambda-algebra for Moggi's partial lambda-calculus. These models are shown to be equivalent to the originally described categorical models via the global element construction; the proof makes use of a previously introduced construction of classifying categories. The set-theoretic semantics thus obtained is the foundation of the higher order algebraic specification language HasCASL, which combines specification and functional programming.