@Article{Schroder05b,
  author = {Lutz Schr{\"o}der},
  title = {The {HasCASL} Prologue - Categorical Syntax and Semantics of the Partial {$\lambda$}-calculus},
  year = {2006},
  journal = {Theoret. Comput. Sci.},
  volume = {353},
  pages = {1-25},
  keywords = {partial lambda-calculus partial cartesian closed category Henkin model HasCASL CASL},
  url = {http://dx.doi.org/10.1016/j.tcs.2005.06.037},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/prologue.pdf"> [preprint] </a>},
  psurl = {http://www8.informatik.uni-erlangen.de/~schroeder/papers/prologue.ps},
  abstract = {We develop the semantic foundations of the specification language HasCASL, which combines algebraic specification and functional programming on the basis of Moggi's partial {$\lambda$}-calculus. Generalizing Lambek's classical equivalence between the simply typed {$\lambda$}-calculus and cartesian closed categories, we establish an equivalence between partial cartesian closed categories (pccc's) and partial {$\lambda$}-theories. Building on these results, 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 in pccc's via the global element construction. The semantics of HasCASL is defined in terms of syntactic {$\lambda$}-algebras. Correlations between logics and classes of categories facilitate reasoning both on the logical and on the categorical side; as an application, we pinpoint unique choice as the distinctive feature of topos logic (in comparison to intuitionistic higher-order logic of partial functions, which by our results is the logic of pccc's with
equality). Finally, we give some applications of the model-theoretic equivalence result to the semantics of HasCASL and its relation to first-order CASL.
},
}