Computer Science Logic and 8th Kurt Gödel Colloquium Lutz Schröder: Henkin models of the partial lambda-calculus

Welcome and News Host Institutions Calls and Deadlines Program Social Program Registration Location and Venue Accommodation Committees Contact Colocated Events Authors' instructions

Print this page 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. © 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-06-04