
We define (settheoretic) notions of intensional Henkin model and syntactic lambdaalgebra for Moggi's partial lambdacalculus. 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 settheoretic semantics thus obtained is the foundation of the higher order algebraic specification language HasCASL, which combines specification and functional programming.
© 20022003 Kurt Gödel Society, Norbert Preining. 
20030604
 