hets.bib revision 9c3b1fb1952bb78a1942fe612215f940fc8e5f31
@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},
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},
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}
}
@article{RiazanovV02,
author = {Alexandre Riazanov and
Andrei Voronkov},
title = {The design and implementation of {VAMPIRE}},
journal = {AI Communications},
volume = {15},
number = {2-3},
year = {2002},
pages = {91-110},
ee = {http://iospress.metapress.com/openurl.asp?genre=article{\&}issn=0921-7126{\&}volume=15{\&}issue=2{\&}spage=91},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@InProceedings{ZimmerAutexier06,
author = {J{\"u}rgen Zimmer and Serge Autexier},
title = {The {M}ath{S}erve {S}ystem for {S}emantic {W}eb {R}easoning {S}ervices},
booktitle = {3rd IJCAR},
editor = {U. Furbach and N. Shankar},
series = {LNCS 4130},
year = 2006,
publisher = {Springer},
}
@InProceedings{LuettichEA06a,
author = {Klaus L{\"u}ttich and Till Mossakowski},
title = {Reasoning {S}upport for {CASL} with {A}utomated {T}heorem {P}roving {S}ystems},
note = {WADT 2006, Springer LNCS, to appear},
status = {Other}
}
@article{Mossakowski02,
author = {Till Mossakowski},
title = {Relating {\CASL} with Other Specification Languages:
the Institution Level},
year = 2002,
journal = {Theoretical Computer Science},
volume = {286},
pages = {367--475},
}
@ARTICLE{GoguenBurstall92,
AUTHOR = "J. A. Goguen and R. M. Burstall",
TITLE = "Institutions: Abstract Model Theory for Specification and
Programming",
JOURNAL = "Journal of the Association for Computing Machinery",
VOLUME = 39,
PAGES = {95--146},
NOTE = {Predecessor in: LNCS 164, 221--256, 1984.},
YEAR = 1992}
@article{GoguenRosu02,
author = {J. Goguen and G. Ro\c{s}u},
title = {Institution morphisms},
journal = {Formal aspects of computing},
volume = {13},
year = {2002},
pages = {274-307},
}
@unpublished{Habil,
Author = {T. Mossakowski},
Title = {Heterogeneous specification and the heterogeneous tool set},
Note = {Habilitation thesis, University of Bremen},
Year = 2005,
}
@InProceedings{MossakowskiEA06,
author = {Till Mossakowski and Christian Maeder and Klaus L{\"u}ttich},
title = {The {H}eterogeneous {T}ool {S}et},
year = {2007},
editor = {Orna Grumberg and Michael Huth},
booktitle = {TACAS 2007},
publisher = {Springer-Verlag Heidelberg},
series = {Lecture Notes in Computer Science},
volume = {4424},
pages = {519-522},
keywords = {proof heterogeneity logic institution prover theorem integration development graph},
abstract = {Heterogeneous specification becomes more and more important because
complex systems are often specified using multiple viewpoints,
involving multiple formalisms. Moreover, a formal software development
process may lead to a change of formalism during the development.
However, current research in integrated formal methods only deals
with ad-hoc integrations of different formalisms.
The heterogeneous tool set (Hets) is a parsing, static analysis and
proof management tool combining various such tools for individual
specification languages, thus providing a tool for heterogeneous
multi-logic specification. Hets is based on a graph of logics and
languages (formalized as so-called institutions), their tools, and
their translations. This provides a clean semantics of heterogeneous
specification, as well as a corresponding proof calculus. For proof
management, the calculus of development graphs (known from other
large-scale proof management systems) has been adapted to
heterogeneous specification. Development graphs provide an overview of
the (heterogeneous) specification module hierarchy and the current
proof state, and thus may be used for monitoring the overall
correctness of a heterogeneous development.},
status = {Reviewed}
}
@Article{MossakowskiEtAl05,
author = {T. Mossakowski and S. Autexier and D. Hutter},
title = {Development Graphs -- Proof Management for Structured Specifications},
year = {2006},
journal = {Journal of Logic and Algebraic Programming},
volume = {67},
pages = {114-145},
number = {1-2},
keywords = {development graph proof logic institution completeness},
abstract = {Development graphs are a tool for dealing with structured
specifications in a formal program development in order to ease the
management of change and reusing proofs. In this work, we extend
development graphs with hiding (e.g. hidden operations). Hiding is
a particularly difficult to realize operation, since it does not
admit such a good decomposition of the involved specifications as
other structuring operations do. We develop both a semantics and
proof rules for development graphs with hiding. The rules are proven
to be sound, and also complete relative to an oracle for
conservative extensions. We also show that an absolutely complete set
of rules cannot exist.
The whole framework is developed in a way independent of the
underlying logical system (and thus also does not prescribe the
nature of the parts of a specification that may be hidden). We also
show how various other logic independent specification formalisms
can be mapped into development graphs; thus, development graphs can
serve as a kernel formalism for management of proofs and of change.},
issn = {1567-8326},
status = {Reviewed}
}
@Book{blackburn_p-etal:2001a,
author = "Patrick BLackburn and Maarten de Rijke and Yde
Venema",
title = "Modal Logic",
publisher = "Cambridge University Press",
year = "2001",
address = "Cambridge, England",
ISBN = "0 521 52714 7 (pbk)",
topic = "modal-logic;",
}