hets.bib revision a22936ffa58b0b92b957098a1ebc75a22cc48f85
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett author = {L. Schr\"oder and T. Mossakowski and C. Maeder},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett title = {{\HasCASL} -- {I}ntegrated functional specification and programming. {L}anguage Summary},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett note = {Available at \url{http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HasCASL}},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett year = {2003},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett@Article{Schroder05b,
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett author = {Lutz Schr{\"o}der},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett title = {The {HasCASL} Prologue - Categorical Syntax and Semantics of the Partial {$\lambda$}-calculus},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett year = {2006},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett journal = {Theoret. Comput. Sci.},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett volume = {353},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett pages = {1-25},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett keywords = {partial lambda-calculus partial cartesian closed category Henkin model HasCASL CASL},
2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett pdfurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/prologue.pdf},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett psurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/prologue.ps},
2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett 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
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettequality). Finally, we give some applications of the model-theoretic equivalence result to the semantics of HasCASL and its relation to first-order CASL.
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett status = {Reviewed}
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett@unpublished{Schroder-habil,
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett author = {Lutz Schr\"oder},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett title = {Higher order and reactive algebraic specification and development},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett school = {University of Bremen},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett year = {2005},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett note = {Summary of papers constituting a cumulative habilitation thesis; available under \url{http://www.informatik.uni-bremen.de/~lschrode/papers/Summary.pdf}},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett@Misc{ModalCASL,
2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett author = {T. Mossakowski},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett title = {Modal{CASL} - Specification with Multi-Modal Logics. Language Summary},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett year = {2004},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett keywords = {modal logic CASL},
2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett pdfurl = {http://www.tzi.de/~till/papers/Modal-Summary.pdf},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett psurl = {http://www.tzi.de/~till/papers/Modal-Summary.ps},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett abstract = {ModalCASL extends CASL by modal operators. Syntax for ordinary
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett modalities, multi-modal logics as well as term-modal
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett logic (also covering dynamic logic) is provided.
2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett Specific modal logics can be obtained via restrictions to
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sublanguages.
34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettThis document provides a detailed definition of the ModalCASL syntax
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettand an informal description of the semantics, building on the existing
34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettCASL Summary.},
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett status = {Other}
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett@article{RiazanovV02,
8e97dcf353ac3afc326ecfd167abd47897215436Andy Gimblett author = {Alexandre Riazanov and
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Andrei Voronkov},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett title = {The design and implementation of {VAMPIRE}},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett journal = {AI Communications},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett volume = {15},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett number = {2-3},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett year = {2002},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett pages = {91-110},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett ee = {http://iospress.metapress.com/openurl.asp?genre=article{\&}issn=0921-7126{\&}volume=15{\&}issue=2{\&}spage=91},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett bibsource = {DBLP, http://dblp.uni-trier.de}
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett@InProceedings{ZimmerAutexier06,
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettauthor = {J{\"u}rgen Zimmer and Serge Autexier},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimbletttitle = {The {M}ath{S}erve {S}ystem for {S}emantic {W}eb {R}easoning {S}ervices},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettbooktitle = {3rd IJCAR},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimbletteditor = {U. Furbach and N. Shankar},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettseries = {LNCS 4130},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettpublisher = {Springer},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett@INPROCEEDINGS{LuettichEA06a,
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett author = {Klaus L{\"u}ttich and Till Mossakowski},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett title = {Reasoning {S}upport for {CASL} with {A}utomated {T}heorem {P}roving {S}ystems},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett pages = {74--91},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett crossref={WADT06},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett url = {http://www.informatik.uni-bremen.de/~till/papers/casl2spass.pdf}}
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett@PROCEEDINGS{WADT06,
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett booktitle = {WADT 2006},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett title = {WADT 2006},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett year = {2007},
2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett editor = {J. Fiadeiro},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett series = {LNCS},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett number = {4409},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett publisher = {Springer}}
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett@article{Mossakowski02,
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett author = {Till Mossakowski},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett title = {Relating {\CASL} with Other Specification Languages:
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett the Institution Level},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett journal = {Theoretical Computer Science},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett volume = {286},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett pages = {367--475},
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett@ARTICLE{GoguenBurstall92,
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy GimblettAUTHOR = "J. A. Goguen and R. M. Burstall",
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy GimblettTITLE = "Institutions: Abstract Model Theory for Specification and
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettJOURNAL = "Journal of the Association for Computing Machinery",
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy GimblettPAGES = {95--146},
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy GimblettNOTE = {Predecessor in: LNCS 164, 221--256, 1984.},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett@article{GoguenRosu02,
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett author = {J. Goguen and G. Ro\c{s}u},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett title = {Institution morphisms},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett journal = {Formal aspects of computing},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett volume = {13},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett year = {2002},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett pages = {274-307},
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett@unpublished{Habil,
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Author = {T. Mossakowski},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Title = {Heterogeneous specification and the heterogeneous tool set},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Note = {Habilitation thesis, University of Bremen},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett@InProceedings{MossakowskiEA06,
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett author = {Till Mossakowski and Christian Maeder and Klaus L{\"u}ttich},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett title = {The {H}eterogeneous {T}ool {S}et},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett year = {2007},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett editor = {Orna Grumberg and Michael Huth},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett booktitle = {TACAS 2007},
29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy Gimblett publisher = {Springer-Verlag Heidelberg},
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett series = {Lecture Notes in Computer Science},
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett volume = {4424},
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett pages = {519-522},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett keywords = {proof heterogeneity logic institution prover theorem integration development graph},
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett pdfurl = {http://www.tzi.de/~till/papers/hets-tacas-toolpaper.pdf},
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett psurl = {http://www.tzi.de/~till/papers/hets-tacas-toolpaper.ps},
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett abstract = {Heterogeneous specification becomes more and more important because
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettcomplex systems are often specified using multiple viewpoints,
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettinvolving multiple formalisms. Moreover, a formal software development
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettprocess may lead to a change of formalism during the development.
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy GimblettHowever, current research in integrated formal methods only deals
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettwith ad-hoc integrations of different formalisms.
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy GimblettThe heterogeneous tool set (Hets) is a parsing, static analysis and
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblettproof management tool combining various such tools for individual
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblettspecification languages, thus providing a tool for heterogeneous
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblettmulti-logic specification. Hets is based on a graph of logics and
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettlanguages (formalized as so-called institutions), their tools, and
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimbletttheir translations. This provides a clean semantics of heterogeneous
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblettspecification, as well as a corresponding proof calculus. For proof
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettmanagement, the calculus of development graphs (known from other
d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblettlarge-scale proof management systems) has been adapted to
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblettheterogeneous specification. Development graphs provide an overview of
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettthe (heterogeneous) specification module hierarchy and the current
b34e5090387d45b3a35f88eaa23477a83d2a2962Andy Gimblettproof state, and thus may be used for monitoring the overall
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblettcorrectness of a heterogeneous development.},
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett status = {Reviewed}
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett@Article{MossakowskiEtAl05,
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett author = {T. Mossakowski and S. Autexier and D. Hutter},
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett title = {Development Graphs -- Proof Management for Structured Specifications},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett year = {2006},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett journal = {Journal of Logic and Algebraic Programming},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett volume = {67},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett pages = {114-145},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett number = {1-2},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett keywords = {development graph proof logic institution completeness},
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett url = {http://www.sciencedirect.com/science?_ob=GatewayURL&_origin=CONTENTS&_method=citationSearch&_piikey=S1567832605000810&_version=1&md5=7c18897e9ffad42e0649c6b41203f41e},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett psurl = {http://www.tzi.de/~till/papers/dgh_journal.ps},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett abstract = {Development graphs are a tool for dealing with structured
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett specifications in a formal program development in order to ease the
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett management of change and reusing proofs. In this work, we extend
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett development graphs with hiding (e.g. hidden operations). Hiding is
bf7d1ec09971b005fff4133bb8b6964ab7d264e7Andy Gimblett a particularly difficult to realize operation, since it does not
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett admit such a good decomposition of the involved specifications as
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett other structuring operations do. We develop both a semantics and
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett proof rules for development graphs with hiding. The rules are proven
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett to be sound, and also complete relative to an oracle for
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett conservative extensions. We also show that an absolutely complete set
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett of rules cannot exist.
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett The whole framework is developed in a way independent of the
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett underlying logical system (and thus also does not prescribe the
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett nature of the parts of a specification that may be hidden). We also
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett show how various other logic independent specification formalisms
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett can be mapped into development graphs; thus, development graphs can
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett serve as a kernel formalism for management of proofs and of change.},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett issn = {1567-8326},
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett status = {Reviewed}
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett@Book{blackburn_p-etal:2001a,
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett author = "Patrick BLackburn and Maarten de Rijke and Yde
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett title = "Modal Logic",
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett publisher = "Cambridge University Press",
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett year = "2001",
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett address = "Cambridge, England",
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett ISBN = "0 521 52714 7 (pbk)",
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett topic = "modal-logic;",
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett@unpublished{TorriniEtAl07,
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett author = {Paolo Torrini and Christoph L\"{u}th and
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett Christian Maeder and Till Mossakowski},
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett title = {Translating {Haskell} to {Isabelle}},
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett note = {Isabelle workshop at CADE-21},
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett year = {2007},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett@MastersThesis{Groening05,
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett author = {Sonja Gr\"{o}ning},
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett title = {Beweisunterst\"{u}tzung f\"{u}r {HasCASL} in {Isabelle
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett school = {University of Bremen},
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett note = {Diplomarbeit},
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett year = {2005},
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett@InCollection{MossakowskiEtAl07b,
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett author = {Till Mossakowski and Christian Maeder and Klaus L{\"u}ttich},
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett title = {The {H}eterogeneous {T}ool {S}et},
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett year = {2007},
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett editor = {Bernhard Beckert},
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett booktitle = {VERIFY 2007},
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett series = {CEUR Workshop Proceedings},
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett volume = {259},
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett status = {Reviewed}
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett@TechReport{Herbstritt03,
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett author = "Marc Herbstritt",
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett title = "{zChaff}: Modifications and Extensions",
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett institution = "Institut f{\"u}r Informatik, Universit{\"a}t
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett type = "report00188",
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett month = jul # " 17",
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett year = "2003",
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett URL = "ftp://ftp.informatik.uni-freiburg.de/documents/reports/report188/report00188.ps.gz",
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett abstract = "The application of SAT solver in industrial
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett verification tools is mandatory for the successful
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett analysis of problems derived from hardware design,
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett e.g.~Combinational Equivalence Checking (CEC) and
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett Bounded Model Checking (BMC). Moskewicz et al. have
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett developed a new powerful SAT solver in 2001 that
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett outperforms most of the existing publicly available SAT
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett solvers when applied to hard real-world problems,
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett e.g.~from VLSI CAD. There are two versions available of
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett Chaff: {\tt mChaff} and {\tt zChaff}. Both are
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett instances of Chaff, but from the viewpoint of
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett implementation they are totally different since they
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett were developped independently by M.~Moskewicz ({\tt
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett mChaff}) and L. Zhang ({\tt zChaff}). In this paper we
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett concentrate on {\tt zChaff}. We analyze the core issues
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett and propose modifications and extensions.",
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett note = "Thu, 17 Jul 2003 17:11:37 GET",
29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy Gimblett@Misc{Mossakowski04,
29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy Gimblett author = {T. Mossakowski},
29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy Gimblett title = {{HetCASL} - Heterogeneous Specification. Language Summary},
29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy Gimblett year = {2004},
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett pdfurl = {http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HetCASL/HetCASL-Summary.pdf},
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett psurl = {http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HetCASL/HetCASL-Summary.ps},
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett abstract = {Heterogeneous CASL (HetCASL) allows
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettmixing specifications written in different logics (using
29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy Gimbletttranslations between the logics). It extends
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettCASL only at the level of structuring constructs, by adding constructs
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettfor choosing the logic and translating specifications among
29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy Gimblettlogics. HetCASL is needed when combining specifications written in
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettCASL with specifications written in its sublanguages and
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettextensions. HetCASL also allows the integration of logics
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettthat are completely different from the CASL logic.
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettThis document provides a detailed definition of the HetCASL syntax
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettand an informal description of the semantics, building on the existing
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettCASL Summary.},
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett status = {Other}
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett title = "{OMD}oc - An Open Markup Format for Mathematical
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Documents [version 1.2]",
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett author = "Michael Kohlhase",
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett publisher = "Springer",
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett year = "2006",
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett volume = "4180",
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett bibdate = "2006-12-13",
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett ISBN = "3-540-37897-9",
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett series = "Lecture Notes in Computer Science",
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett@Unpublished{SparQ06,
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett author = {Jan Oliver Wallgr\"un and Lutz Frommberger and Frank Dylla and Diedrich Wolter},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett title = {{SparQ} User Manual V0.6.2},
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett note = {University of Bremen},
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett year = {2006},
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett@incollection{TypeClasses,
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett author = {Simon {Peyton Jones} and Mark Jones and Erik Meijer},
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett title = {Type classes: exploring the design space},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett booktitle = {Haskell Workshop},
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett year = {1997},
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett@techreport{Parsec,
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett author = {Daan Leijen and Erik Meijer},
note = {available at \texttt{http://www.haskell.org/ghc}},
pdfurl = {http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/UserGuide.pdf},