by Lutz Schröder
Abstract:
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.
Reference:
Lutz Schröder: Henkin models of the partial $\lambda$-calculus, In Matthias Baaz, Johann Makowsky, eds.: Computer Science Logic, Lecture Notes in Computer Science, vol. 2803, pp. 498–512, Springer; Berlin; http://www.springer.de, 2003. [preprint]
Bibtex Entry:
@InProceedings{Schroder03b,
author = {Lutz Schr{\"o}der},
title = {Henkin models of the partial {$\lambda$}-calculus},
year = {2003},
editor = {Matthias Baaz and Johann Makowsky},
booktitle = {Computer Science Logic},
publisher = {Springer; Berlin; http://www.springer.de},
series = {Lecture Notes in Computer Science},
volume = {2803},
pages = {498--512},
keywords = {HasCASL partial lambda-calculus Henkin models partial cartesian closed categories},
url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2803&spage=498},
comment = {<a href="http://www8.informatik.uni-erlangen.de/~schroeder/papers/henkinpl.ps">[preprint]</a>},
abstract = {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.
},
}