hets.bib revision 2c66eeb1cc9ad264525901f10c35c66638f91865
08ea5f703d2e034f347a7e30ee3cca8a127d9c0eChristian Maeder author = {L. Schr\"oder and T. Mossakowski and C. Maeder},
e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowski title = {{\HasCASL} -- {I}ntegrated functional specification and programming. {L}anguage Summary},
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach note = {Available at \verb?http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/? \verb?CoFI/HasCASL?}},
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski@Article{Schroder05b,
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach author = {Lutz Schr{\"o}der},
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach title = {The {HasCASL} Prologue - Categorical Syntax and Semantics of the Partial {$\lambda$}-calculus},
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach year = {2006},
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder journal = {Theoret. Comput. Sci.},
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach volume = {353},
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach pages = {1-25},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly keywords = {partial lambda-calculus partial cartesian closed category Henkin model HasCASL CASL},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly pdfurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/prologue.pdf},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly psurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/prologue.ps},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly 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
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillyequality). Finally, we give some applications of the model-theoretic equivalence result to the semantics of HasCASL and its relation to first-order CASL.
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly status = {Reviewed}
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly@unpublished{Schroder-habil,
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly author = {Lutz Schr�der},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly title = {Higher order and reactive algebraic specification and development},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly school = {University of Bremen},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly year = {2005},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly note = {summary of papers constituting a cumulative habilitation thesis; available under \url{http://www.informatik.uni-bremen.de/~lschrode/papers/Summary.pdf}},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly@Misc{ModalCASL,
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly author = {T. Mossakowski},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly title = {Modal{CASL} - Specification with Multi-Modal Logics. Language Summary},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly year = {2004},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly keywords = {modal logic CASL},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly pdfurl = {http://www.tzi.de/~till/papers/Modal-Summary.pdf},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly psurl = {http://www.tzi.de/~till/papers/Modal-Summary.ps},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly abstract = {ModalCASL extends CASL by modal operators. Syntax for ordinary
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly modalities, multi-modal logics as well as term-modal
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly logic (also covering dynamic logic) is provided.
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly Specific modal logics can be obtained via restrictions to
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly sublanguages.
bcd914850de931848b86d7728192a149f9c0108bChristian MaederThis document provides a detailed definition of the ModalCASL syntax
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maederand an informal description of the semantics, building on the existing
842ae753ab848a8508c4832ab64296b929167a97Christian MaederCASL Summary.},
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder status = {Other}
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly@article{RiazanovV02,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly author = {Alexandre Riazanov and
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Andrei Voronkov},
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly title = {The design and implementation of {VAMPIRE}},
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder journal = {AI Communications},
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder volume = {15},
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly number = {2-3},
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly year = {2002},
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder pages = {91-110},
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ee = {http://iospress.metapress.com/openurl.asp?genre=article{\&}issn=0921-7126{\&}volume=15{\&}issue=2{\&}spage=91},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly bibsource = {DBLP, http://dblp.uni-trier.de}
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder@InProceedings{ZimmerAutexier06,
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederauthor = {J{\"u}rgen Zimmer and Serge Autexier},
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maedertitle = {The {M}ath{S}erve {S}ystem for {S}emantic {W}eb {R}easoning {S}ervices},
f284db6f4dffd7bf60b82319648efb7bcb9378c9Christian Maederbooktitle = {3rd IJCAR},
f284db6f4dffd7bf60b82319648efb7bcb9378c9Christian Maedereditor = {U. Furbach and N. Shankar},
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettseries = {LNCS 4130},
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederpublisher = {Springer},
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett@InProceedings{LuettichEA06a,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly author = {Klaus L{\"u}ttich and Till Mossakowski},
2650e8a56cc2381719bd2390fdf82402e0c696d8Christian Maeder title = {Reasoning {S}upport for {CASL} with {A}utomated {T}heorem {P}roving {S}ystems},
2650e8a56cc2381719bd2390fdf82402e0c696d8Christian Maeder note = {WADT 2006, Springer LNCS, to appear},
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder status = {Other}
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder@article{Mossakowski02,
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder author = {Till Mossakowski},
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly title = {Relating {\CASL} with Other Specification Languages:
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder the Institution Level},
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder journal = {Theoretical Computer Science},
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder volume = {286},
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder pages = {367--475},
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly@ARTICLE{GoguenBurstall92,
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederAUTHOR = "J. A. Goguen and R. M. Burstall",
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyTITLE = "Institutions: Abstract Model Theory for Specification and
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyJOURNAL = "Journal of the Association for Computing Machinery",
842ae753ab848a8508c4832ab64296b929167a97Christian MaederPAGES = {95--146},
842ae753ab848a8508c4832ab64296b929167a97Christian MaederNOTE = {Predecessor in: LNCS 164, 221--256, 1984.},
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly@article{GoguenRosu02,
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder author = {J. Goguen and G. Ro\c{s}u},
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder title = {Institution morphisms},
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder journal = {Formal aspects of computing},
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder volume = {13},
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder year = {2002},
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder pages = {274-307},
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder@unpublished{Habil,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Author = {T. Mossakowski},
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Title = {Heterogeneous specification and the heterogeneous tool set},
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Note = {Habilitation thesis, University of Bremen},
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly@InProceedings{MossakowskiEA06,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly author = {Till Mossakowski and Christian Maeder and Klaus L{\"u}ttich},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly title = {The {H}eterogeneous {T}ool {S}et},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly year = {2007},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly editor = {Orna Grumberg and Michael Huth},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly booktitle = {TACAS 2007},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly publisher = {Springer-Verlag Heidelberg},
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett series = {Lecture Notes in Computer Science},
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly volume = {4424},
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly pages = {519-522},
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly keywords = {proof heterogeneity logic institution prover theorem integration development graph},
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett pdfurl = {http://www.tzi.de/~till/papers/hets-tacas-toolpaper.pdf},
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett psurl = {http://www.tzi.de/~till/papers/hets-tacas-toolpaper.ps},
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly abstract = {Heterogeneous specification becomes more and more important because
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillycomplex systems are often specified using multiple viewpoints,
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederinvolving multiple formalisms. Moreover, a formal software development
2650e8a56cc2381719bd2390fdf82402e0c696d8Christian Maederprocess may lead to a change of formalism during the development.
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederHowever, current research in integrated formal methods only deals
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillywith ad-hoc integrations of different formalisms.
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyThe heterogeneous tool set (Hets) is a parsing, static analysis and
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyproof management tool combining various such tools for individual
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederspecification languages, thus providing a tool for heterogeneous
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettmulti-logic specification. Hets is based on a graph of logics and
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillylanguages (formalized as so-called institutions), their tools, and
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillytheir translations. This provides a clean semantics of heterogeneous
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillyspecification, as well as a corresponding proof calculus. For proof
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillymanagement, the calculus of development graphs (known from other
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillylarge-scale proof management systems) has been adapted to
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillyheterogeneous specification. Development graphs provide an overview of
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillythe (heterogeneous) specification module hierarchy and the current
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reillyproof state, and thus may be used for monitoring the overall
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reillycorrectness of a heterogeneous development.},
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly status = {Reviewed}
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly@Article{MossakowskiEtAl05,
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly author = {T. Mossakowski and S. Autexier and D. Hutter},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly title = {Development Graphs -- Proof Management for Structured Specifications},
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly year = {2006},
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly journal = {Journal of Logic and Algebraic Programming},
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly volume = {67},
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly pages = {114-145},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly number = {1-2},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly keywords = {development graph proof logic institution completeness},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly url = {http://www.sciencedirect.com/science?_ob=GatewayURL&_origin=CONTENTS&_method=citationSearch&_piikey=S1567832605000810&_version=1&md5=7c18897e9ffad42e0649c6b41203f41e},
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly psurl = {http://www.tzi.de/~till/papers/dgh_journal.ps},
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly abstract = {Development graphs are a tool for dealing with structured
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly specifications in a formal program development in order to ease the
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly management of change and reusing proofs. In this work, we extend
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly development graphs with hiding (e.g. hidden operations). Hiding is
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly a particularly difficult to realize operation, since it does not
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly admit such a good decomposition of the involved specifications as
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly other structuring operations do. We develop both a semantics and
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly proof rules for development graphs with hiding. The rules are proven
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly to be sound, and also complete relative to an oracle for
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly conservative extensions. We also show that an absolutely complete set
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly of rules cannot exist.
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly The whole framework is developed in a way independent of the
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly underlying logical system (and thus also does not prescribe the
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly nature of the parts of a specification that may be hidden). We also
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly show how various other logic independent specification formalisms
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly can be mapped into development graphs; thus, development graphs can
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly serve as a kernel formalism for management of proofs and of change.},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly issn = {1567-8326},
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly status = {Reviewed}
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly@Book{blackburn_p-etal:2001a,
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly author = "Patrick BLackburn and Maarten de Rijke and Yde
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly title = "Modal Logic",
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly publisher = "Cambridge University Press",
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett year = "2001",
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett address = "Cambridge, England",
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett ISBN = "0 521 52714 7 (pbk)",
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett topic = "modal-logic;",
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder@unpublished{TorriniEtAl07,
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'Reilly author = {Paolo Torrini and Christoph L\"{u}th and
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder Christian Maeder and Till Mossakowski},
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly title = {Translating Haskell to Isabelle},
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly note = {submitted for publication},
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder@MastersThesis{Groening05,
929190acb9f2b2f5857dce841c5a389710895515Andy Gimblett author = {Sonja Gr\"{o}ning},
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly title = {Beweisunterst\"{u}tzung f\"{u}r HasCASL in Isabelle
cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'Reilly school = {University of Bremen},
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly note = {Diplomarbeit},
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly year = {2005},