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

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

}

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

pdfurl = {http://www.tzi.de/~till/papers/hets-tacas-toolpaper.pdf},

psurl = {http://www.tzi.de/~till/papers/hets-tacas-toolpaper.ps},

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

url = {http://www.sciencedirect.com/science?_ob=GatewayURL&_origin=CONTENTS&_method=citationSearch&_piikey=S1567832605000810&_version=1&md5=7c18897e9ffad42e0649c6b41203f41e},

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

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;",

}

@unpublished{TorriniEtAl07,

author = {Paolo Torrini and Christoph L\"{u}th and

Christian Maeder and Till Mossakowski},

title = {Translating Haskell to Isabelle},

note = {submitted for publication},

}

@MastersThesis{Groening05,

author = {Sonja Gr\"{o}ning},

title = {Beweisunterst\"{u}tzung f\"{u}r HasCASL in Isabelle

/HOL},

school = {University of Bremen},

note = {Diplomarbeit},

year = {2005},

}