@unpublished{HasCASL/Summary,

author = {L. Schr\"oder and T. Mossakowski and C. Maeder},

title = {{\HasCASL} -- {I}ntegrated functional specification and programming. {L}anguage Summary},

note = {Available at \verb?http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/? \verb?CoFI/HasCASL?}},

year = {2003},

@Book{PeytonJones03,

editor = {S. Peyton-Jones},

title = {{Haskell} 98 Language and Libraries ---

The Revised Report},

publisher = {Cambridge},

year = {2003},

note = {also: J.\ Funct.\ Programming {{\bf 13}} (2003)}

}

@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},

pdfurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/prologue.pdf},

psurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/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.

},

status = {Reviewed}

}

@unpublished{Schroder-habil,

author = {Lutz Schr�der},

title = {Higher order and reactive algebraic specification and development},

school = {University of Bremen},

year = {2005},

note = {summary of papers constituting a cumulative habilitation thesis; available under \url{http://www.informatik.uni-bremen.de/~lschrode/papers/Summary.pdf}},

}

@Misc{ModalCASL,

author = {T. Mossakowski},

title = {Modal{CASL} - Specification with Multi-Modal Logics. Language Summary},

year = {2004},

keywords = {modal logic CASL},

pdfurl = {http://www.tzi.de/~till/papers/Modal-Summary.pdf},

psurl = {http://www.tzi.de/~till/papers/Modal-Summary.ps},

abstract = {ModalCASL extends CASL by modal operators. Syntax for ordinary

modalities, multi-modal logics as well as term-modal

logic (also covering dynamic logic) is provided.

Specific modal logics can be obtained via restrictions to

sublanguages.

This document provides a detailed definition of the ModalCASL syntax

and an informal description of the semantics, building on the existing

CASL Summary.},

status = {Other}

}