hets.bib revision 89118fd658073a87eddf4ead4bb63c6adb30550d
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski author = {L. Schr\"oder and T. Mossakowski and C. Maeder},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski title = {{\HasCASL} -- {I}ntegrated functional specification and programming. {L}anguage Summary},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski note = {Available at \verb?http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/? \verb?CoFI/HasCASL?}},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski year = {2003},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski@Book{PeytonJones03,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski editor = {S. Peyton-Jones},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski title = {{Haskell} 98 Language and Libraries ---
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe Revised Report},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski publisher = {Cambridge},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski year = {2003},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski note = {also: J.\ Funct.\ Programming {{\bf 13}} (2003)}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski@Article{Schroder05b,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski author = {Lutz Schr{\"o}der},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski title = {The {HasCASL} Prologue - Categorical Syntax and Semantics of the Partial {$\lambda$}-calculus},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski year = {2006},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski journal = {Theoret. Comput. Sci.},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski volume = {353},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski pages = {1-25},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski keywords = {partial lambda-calculus partial cartesian closed category Henkin model HasCASL CASL},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski pdfurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/prologue.pdf},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski psurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/prologue.ps},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski 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
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiequality). Finally, we give some applications of the model-theoretic equivalence result to the semantics of HasCASL and its relation to first-order CASL.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski status = {Reviewed}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski@unpublished{Schroder-habil,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski author = {Lutz Schr�der},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski title = {Higher order and reactive algebraic specification and development},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski school = {University of Bremen},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski year = {2005},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski note = {summary of papers constituting a cumulative habilitation thesis; available under \url{http://www.informatik.uni-bremen.de/~lschrode/papers/Summary.pdf}},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski@Misc{ModalCASL,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski author = {T. Mossakowski},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski title = {Modal{CASL} - Specification with Multi-Modal Logics. Language Summary},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski year = {2004},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski keywords = {modal logic CASL},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski pdfurl = {http://www.tzi.de/~till/papers/Modal-Summary.pdf},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski psurl = {http://www.tzi.de/~till/papers/Modal-Summary.ps},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski abstract = {ModalCASL extends CASL by modal operators. Syntax for ordinary
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski modalities, multi-modal logics as well as term-modal
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski logic (also covering dynamic logic) is provided.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Specific modal logics can be obtained via restrictions to
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski sublanguages.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThis document provides a detailed definition of the ModalCASL syntax
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiand an informal description of the semantics, building on the existing
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCASL Summary.},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski status = {Other}