| Publication type: |
Article |
| Author: |
Lutz Schröder |
| Title: |
The HasCASL Prologue - Categorical Syntax and Semantics of the Partial λ-calculus |
| Volume: |
353 |
| Page(s): |
1 – 25 |
| Journal: |
Theoret. Comput. Sci. |
| Year published: |
2006 |
| 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 λ-calculus. Generalizing Lambek's classical equivalence between the simply typed λ-calculus and cartesian closed categories, we establish an equivalence between partial cartesian closed categories (pccc's) and partial λ-theories. Building on these results, we define (set-theoretic) notions of intensional Henkin model and syntactic λ-algebra for Moggi's partial λ-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 λ-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.
|
| Internet: |
http://dx.doi.org/10.1016/j.tcs.2005.06.037 |
| PDF Version: |
http://www.informatik.uni-bremen.de/~lschrode/hascasl/prologue.pdf |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~lschrode/hascasl/prologue.ps |
| Keywords: |
partial lambda-calculus partial cartesian closed category Henkin model HasCASL CASL |
| Status: |
Reviewed |
| Last updated: |
18. 06. 2008 |
