@MastersThesis{Codruta10,
author = {Codru\c{t}a G{\^i}rlea},
title = {An Extended Modal Logic Institution},
school = {Department of Computer Science, University of Bremen},
year = 2010}
@book{Sannella12,
author = {Donald Sannella and
Andrzej Tarlecki},
title = {Foundations of Algebraic Specification and Formal Software
Development},
publisher = {Springer},
series = {EATCS Monographs on theoretical computer science},
year = {2012},
isbn = {978-3-642-17335-6},
pages = {I-XVI, 1-581},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@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 \url{http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/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},
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\"oder},
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},
pages = {74--91},
crossref={WADT06},
@PROCEEDINGS{WADT06,
booktitle = {WADT 2006},
title = {WADT 2006},
year = {2007},
editor = {J. Fiadeiro},
series = {LNCS},
number = {4409},
publisher = {Springer}}
@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;",
}
@unpublished{TorriniEtAl07,
author = {Paolo Torrini and Christoph L\"{u}th and
Christian Maeder and Till Mossakowski},
title = {Translating {Haskell} to {Isabelle}},
note = {Isabelle workshop at CADE-21},
year = {2007},
}
@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},
}
@InCollection{MossakowskiEtAl07b,
author = {Till Mossakowski and Christian Maeder and Klaus L{\"u}ttich},
title = {The {H}eterogeneous {T}ool {S}et},
year = {2007},
editor = {Bernhard Beckert},
booktitle = {VERIFY 2007},
series = {CEUR Workshop Proceedings},
volume = {259},
status = {Reviewed}
}
@TechReport{Herbstritt03,
author = "Marc Herbstritt",
title = "{zChaff}: Modifications and Extensions",
institution = "Institut f{\"u}r Informatik, Universit{\"a}t
Freiburg",
type = "report00188",
month = jul # " 17",
year = "2003",
abstract = "The application of SAT solver in industrial
verification tools is mandatory for the successful
analysis of problems derived from hardware design,
e.g.~Combinational Equivalence Checking (CEC) and
Bounded Model Checking (BMC). Moskewicz et al. have
developed a new powerful SAT solver in 2001 that
outperforms most of the existing publicly available SAT
solvers when applied to hard real-world problems,
e.g.~from VLSI CAD. There are two versions available of
Chaff: {\tt mChaff} and {\tt zChaff}. Both are
instances of Chaff, but from the viewpoint of
implementation they are totally different since they
were developped independently by M.~Moskewicz ({\tt
mChaff}) and L. Zhang ({\tt zChaff}). In this paper we
concentrate on {\tt zChaff}. We analyze the core issues
and propose modifications and extensions.",
note = "Thu, 17 Jul 2003 17:11:37 GET",
}
@Misc{Mossakowski04,
author = {T. Mossakowski},
title = {{HetCASL} -- Heterogeneous Specification. {Language} Summary},
year = {2004},
pdfurl = {http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HetCASL/HetCASL-Summary.pdf},
psurl = {http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HetCASL/HetCASL-Summary.ps},
abstract = {Heterogeneous CASL (HetCASL) allows
mixing specifications written in different logics (using
translations between the logics). It extends
CASL only at the level of structuring constructs, by adding constructs
for choosing the logic and translating specifications among
logics. HetCASL is needed when combining specifications written in
CASL with specifications written in its sublanguages and
extensions. HetCASL also allows the integration of logics
that are completely different from the CASL logic.
This document provides a detailed definition of the HetCASL syntax
and an informal description of the semantics, building on the existing
CASL Summary.},
status = {Other}
}
@Book{books/sp/Kohlhase06,
title = "{OMD}oc -- An Open Markup Format for Mathematical
Documents [version 1.2]",
author = "Michael Kohlhase",
publisher = "Springer",
year = "2006",
volume = "4180",
bibdate = "2006-12-13",
ISBN = "3-540-37897-9",
series = "Lecture Notes in Computer Science",
URL = "http://dx.doi.org/10.1007/11826095",
}
@Unpublished{SparQ06,
author = {Jan Oliver Wallgr\"un and Lutz Frommberger and Frank Dylla and Diedrich Wolter},
title = {{SparQ} User Manual V0.6.2},
note = {University of Bremen},
year = {2006},
},
}
@incollection{TypeClasses,
author = {Simon {Peyton Jones} and Mark Jones and Erik Meijer},
title = {Type classes: exploring the design space},
booktitle = {Haskell Workshop},
year = {1997},
}
@techreport{Parsec,
author = {Daan Leijen and Erik Meijer},
title = {Parsec: Direct Style Monadic Parser Combinators for the Real World},
note = {UU-CS-2001-35},
school = {Departement of Computer Science, Universiteit Utrecht},
}
@unpublished{GHC,
title = {The {G}lasgow {H}askell compiler},
note = {available at \texttt{http://www.haskell.org/ghc}},
}
@Article{Roggenbach06,
author = {M. Roggenbach},
title = {{CSP-CASL} - A new integration of process algebra and algebraic specification},
journal = {Theoretical Computer Science},
year = {2006},
volume = {354},
number = {1},
pages = {42--71},
}
@article{VSE00,
author = {Autexier, S. and Hutter, D. and Langenstein, B. and Mantel, H. and
Rock, G. and Schairer, A. and Stephan, W. and Vogt, R. and Wolpers, A.},
title = {{VSE}: Formal methods meet industrial needs},
journal = {International Journal on Software Tools for Technology Transfer, Sp
ecial issue on Mechanized Theorem Proving for Technology},
volume = {3},
number = {1},
publisher = {Springer},
month = {september},
year = {2000},
}
@Misc{HetsUserGuide,
author = {Till Mossakowski, Christian Maeder, Mihai Codescu},
title = {Hets User Guide},
year = {2011},
pdfurl = {http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/UserGuide.pdf},
note = {\url{http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/UserGuide.pdf}},
}
@inproceedings{DBLP:conf/cade/BenzmullerRS08,
author = {Christoph Benzm{\"u}ller and
Florian Rabe and
Geoff Sutcliffe},
title = {{THF0} -- The Core of the {TPTP} Language for Higher-Order Logic},
booktitle = {Automated Reasoning, 4th International Joint Conference,
IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings},
pages = {491-506},
editor = {Alessandro Armando and
Peter Baumgartner and
Gilles Dowek},
bibsource = {DBLP, http://dblp.uni-trier.de},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5195},
year = {2008},
isbn = {978-3-540-71069-1},
}
@inproceedings{DBLP:conf/lpar/Sutcliffe10,
author = {Geoff Sutcliffe},
title = {The {TPTP} World -- Infrastructure for Automated Reasoning},
year = {2010},
pages = {1-12},
bibsource = {DBLP, http://dblp.uni-trier.de},
editor = {Edmund M. Clarke and
Andrei Voronkov},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning
- 16th International Conference, LPAR-16, Dakar, Senegal,
April 25-May 1, 2010, Revised Selected Papers},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6355},
isbn = {978-3-642-17510-7},
}
@Article{Schulz:AICOM-2002,
author = {S. Schulz},
title = {{E -- A Brainiac Theorem Prover}},
journal = {Journal of AI Communications},
year = {2002},
volume = {15},
number = {2/3},
pages = {111--126},
annote = {StS},
}
@inproceedings{DBLP:conf/cade/PelzerW07,
author = {Bj{\"o}rn Pelzer and
Christoph Wernhard},
title = {System Description: E-KRHyper},
year = {2007},
pages = {508--513},
bibsource = {DBLP, http://dblp.uni-trier.de},
editor = {Frank Pfenning},
booktitle = {Automated Deduction - CADE-21, 21st International Conference
on Automated Deduction, Bremen, Germany, July 17-20, 2007,
Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4603},
isbn = {978-3-540-73594-6},
}
@online{hets-library,crossref={hets-library:base},
url = {http://www.cofi.info/Libraries},
}
@misc{hets-library:URL,crossref={hets-library:base},
howpublished = {\url{http://www.cofi.info/Libraries}},
}
@misc{hets-library:base,
title = {Hets Library},
}
@InProceedings{Baumgartner:etal:Darwin:IJAIT:2005,
author = {Peter Baumgartner and Alexander Fuchs and Cesare Tinelli},
title = "{I}mplementing the {M}odel {E}volution {C}alculus",
booktitle = {{S}pecial {I}ssue of the {I}nternational {J}ournal of
{A}rtificial {I}ntelligence {T}ools ({IJAIT})},
year = {2005},
volume = 15,
number = 1,
editor = {Stephan Schulz and Geoff Sutcliffe and Tanel Tammet},
series = {{I}nternational {J}ournal of {A}rtificial {I}ntelligence {T}ools},
abstract = "Darwin is the first implementation of the Model Evolution Calculus
by Baumgartner and Tinelli.
The Model Evolution Calculus lifts the DPLL procedure to first-order logic.
Darwin is meant to be a fast and clean implementation of the calculus,
showing its effectiveness and providing a base for
further improvements and extensions.
Based on a brief summary of the Model Evolution Calculus, we
describe in the main part of the paper Darwin's proof procedure and
its data structures and algorithms, discussing the main design
decisions and features that influence Darwin's performance. We also
report on practical experiments carried out with problems from the
CASC-J2 system competition and parts of the TPTP Problem Library,
and compare the results with those of other state-of-the-art theorem provers.",
note = {Preprint.}
}
@inproceedings{DBLP:conf/calco/NevesMMB13,
author = {Renato Neves and
Alexandre Madeira and
Manuel A. Martins and
Lu\'{\i}s Soares Barbosa},
title = {Hybridisation at Work},
booktitle = {CALCO},
year = {2013},
pages = {340-345},
crossref = {DBLP:conf/calco/2013},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/calco/2013,
editor = {Reiko Heckel and
Stefan Milius},
title = {Algebra and Coalgebra in Computer Science - 5th International
Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013.
Proceedings},
booktitle = {CALCO},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8089},
year = {2013},
isbn = {978-3-642-40205-0},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/calco/MartinsMDB11,
author = {Manuel A. Martins and
Alexandre Madeira and
Razvan Diaconescu and
Lu\'{\i}s Soares Barbosa},
title = {Hybridization of Institutions},
booktitle = {CALCO},
year = {2011},
pages = {283-297},
crossref = {DBLP:conf/calco/2011},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/calco/2011,
editor = {Andrea Corradini and
Bartek Klin and
Corina C\^{\i}rstea},
title = {Algebra and Coalgebra in Computer Science - 4th International
Conference, CALCO 2011, Winchester, UK, August 30 - September
2, 2011. Proceedings},
booktitle = {CALCO},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6859},
year = {2011},
isbn = {978-3-642-22943-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}