4865N/A author = {L. Schr\"oder and T. Mossakowski and C. Maeder},
4865N/A title = {{\HasCASL} -- {I}ntegrated functional specification and programming. {L}anguage Summary},
4865N/A author = {Lutz Schr{\"o}der},
4865N/A title = {The {HasCASL} Prologue - Categorical Syntax and Semantics of the Partial {$\lambda$}-calculus},
4865N/A journal = {Theoret. Comput. Sci.},
4865N/A keywords = {partial lambda-calculus partial cartesian closed category Henkin model HasCASL CASL},
4865N/A 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
4865N/Aequality). Finally, we give some applications of the model-theoretic equivalence result to the semantics of HasCASL and its relation to first-order CASL.
4865N/A@unpublished{Schroder-habil,
4865N/A author = {Lutz Schr\"oder},
4865N/A title = {Higher order and reactive algebraic specification and development},
4865N/A school = {University of Bremen},
4865N/A title = {Modal{CASL} - Specification with Multi-Modal Logics. Language Summary},
4865N/A keywords = {modal logic CASL},
4865N/A abstract = {ModalCASL extends CASL by modal operators. Syntax for ordinary
4865N/A modalities, multi-modal logics as well as term-modal
4865N/A logic (also covering dynamic logic) is provided.
4865N/A Specific modal logics can be obtained via restrictions to
4865N/AThis document provides a detailed definition of the ModalCASL syntax
4865N/Aand an informal description of the semantics, building on the existing
4865N/A author = {Alexandre Riazanov and
4865N/A title = {The design and implementation of {VAMPIRE}},
4865N/A journal = {AI Communications},
4865N/A@InProceedings{ZimmerAutexier06,
4865N/Aauthor = {J{\"u}rgen Zimmer and Serge Autexier},
4865N/Atitle = {The {M}ath{S}erve {S}ystem for {S}emantic {W}eb {R}easoning {S}ervices},
4865N/Aeditor = {U. Furbach and N. Shankar},
4865N/A@InProceedings{LuettichEA06a,
4865N/A author = {Klaus L{\"u}ttich and Till Mossakowski},
4865N/A title = {Reasoning {S}upport for {CASL} with {A}utomated {T}heorem {P}roving {S}ystems},
4865N/A note = {WADT 2006, Springer LNCS, to appear},
4865N/A author = {Till Mossakowski},
4865N/A title = {Relating {\CASL} with Other Specification Languages:
4865N/A journal = {Theoretical Computer Science},
4865N/AAUTHOR = "J. A. Goguen and R. M. Burstall",
4865N/ATITLE = "Institutions: Abstract Model Theory for Specification and
4865N/AJOURNAL = "Journal of the Association for Computing Machinery",
4865N/ANOTE = {Predecessor in: LNCS 164, 221--256, 1984.},
4865N/A author = {J. Goguen and G. Ro\c{s}u},
4865N/A title = {Institution morphisms},
4865N/A journal = {Formal aspects of computing},
4865N/A Title = {Heterogeneous specification and the heterogeneous tool set},
4865N/A Note = {Habilitation thesis, University of Bremen},
4865N/A@InProceedings{MossakowskiEA06,
4865N/A author = {Till Mossakowski and Christian Maeder and Klaus L{\"u}ttich},
4865N/A title = {The {H}eterogeneous {T}ool {S}et},
4865N/A editor = {Orna Grumberg and Michael Huth},
4865N/A publisher = {Springer-Verlag Heidelberg},
4865N/A series = {Lecture Notes in Computer Science},
4865N/A keywords = {proof heterogeneity logic institution prover theorem integration development graph},
4865N/A abstract = {Heterogeneous specification becomes more and more important because
4865N/Acomplex systems are often specified using multiple viewpoints,
4865N/Ainvolving multiple formalisms. Moreover, a formal software development
4865N/Aprocess may lead to a change of formalism during the development.
4865N/AHowever, current research in integrated formal methods only deals
4865N/Awith ad-hoc integrations of different formalisms.
4865N/AThe heterogeneous tool set (Hets) is a parsing, static analysis and
4865N/Aproof management tool combining various such tools for individual
4865N/Aspecification languages, thus providing a tool for heterogeneous
4865N/Amulti-logic specification. Hets is based on a graph of logics and
4865N/Alanguages (formalized as so-called institutions), their tools, and
4865N/Atheir translations. This provides a clean semantics of heterogeneous
4865N/Aspecification, as well as a corresponding proof calculus. For proof
4865N/Amanagement, the calculus of development graphs (known from other
4865N/Alarge-scale proof management systems) has been adapted to
4865N/Aheterogeneous specification. Development graphs provide an overview of
4865N/Athe (heterogeneous) specification module hierarchy and the current
4865N/Aproof state, and thus may be used for monitoring the overall
4865N/Acorrectness of a heterogeneous development.},
4865N/A author = {T. Mossakowski and S. Autexier and D. Hutter},
4865N/A title = {Development Graphs -- Proof Management for Structured Specifications},
4865N/A journal = {Journal of Logic and Algebraic Programming},
4865N/A keywords = {development graph proof logic institution completeness},
4865N/A abstract = {Development graphs are a tool for dealing with structured
4865N/A specifications in a formal program development in order to ease the
4865N/A management of change and reusing proofs. In this work, we extend
4865N/A development graphs with hiding (
e.g. hidden operations). Hiding is
4865N/A a particularly difficult to realize operation, since it does not
4865N/A admit such a good decomposition of the involved specifications as
4865N/A other structuring operations do. We develop both a semantics and
4865N/A proof rules for development graphs with hiding. The rules are proven
4865N/A to be sound, and also complete relative to an oracle for
4865N/A conservative extensions. We also show that an absolutely complete set
4865N/A The whole framework is developed in a way independent of the
4865N/A underlying logical system (and thus also does not prescribe the
4865N/A nature of the parts of a specification that may be hidden). We also
4865N/A show how various other logic independent specification formalisms
4865N/A can be mapped into development graphs; thus, development graphs can
4865N/A serve as a kernel formalism for management of proofs and of change.},
4865N/A@Book{blackburn_p-etal:2001a,
4865N/A author = "Patrick BLackburn and Maarten de Rijke and Yde
4865N/A publisher = "Cambridge University Press",
4865N/A address = "Cambridge, England",
4865N/A ISBN = "0 521 52714 7 (pbk)",
4865N/A author = {Paolo Torrini and Christoph L\"{u}th and
4865N/A Christian Maeder and Till Mossakowski},
4865N/A title = {Translating {Haskell} to {Isabelle}},
4865N/A note = {Isabelle workshop at CADE-21},
4865N/A author = {Sonja Gr\"{o}ning},
4865N/A title = {Beweisunterst\"{u}tzung f\"{u}r {HasCASL} in {Isabelle
4865N/A school = {University of Bremen},
4865N/A@InCollection{MossakowskiEtAl07b,
4865N/A author = {Till Mossakowski and Christian Maeder and Klaus L{\"u}ttich},
4865N/A title = {The {H}eterogeneous {T}ool {S}et},
4865N/A editor = {Bernhard Beckert},
4865N/A series = {CEUR Workshop Proceedings},
4865N/A crossref = {MossakowskiEA06},
4865N/A author = "Marc Herbstritt",
4865N/A title = "{zChaff}: Modifications and Extensions",
4865N/A institution = "Institut f{\"u}r Informatik, Universit{\"a}t
4865N/A abstract = "The application of SAT solver in industrial
4865N/A verification tools is mandatory for the successful
4865N/A analysis of problems derived from hardware design,
4865N/A e.g.~Combinational Equivalence Checking (CEC) and
4865N/A Bounded Model Checking (BMC). Moskewicz et al. have
4865N/A developed a new powerful SAT solver in 2001 that
4865N/A outperforms most of the existing publicly available SAT
4865N/A solvers when applied to hard real-world problems,
4865N/A e.g.~from VLSI CAD. There are two versions available of
4865N/A Chaff: {\tt mChaff} and {\tt zChaff}. Both are
4865N/A instances of Chaff, but from the viewpoint of
4865N/A implementation they are totally different since they
4865N/A were developped independently by M.~Moskewicz ({\tt
4865N/A mChaff}) and L. Zhang ({\tt zChaff}). In this paper we
4865N/A concentrate on {\tt zChaff}. We analyze the core issues
4865N/A and propose modifications and extensions.",
4865N/A note = "Thu, 17 Jul 2003 17:11:37 GET",
4865N/A title = {{HetCASL} - Heterogeneous Specification. Language Summary},
4865N/A abstract = {Heterogeneous CASL (HetCASL) allows
4865N/Amixing specifications written in different logics (using
4865N/Atranslations between the logics). It extends
4865N/ACASL only at the level of structuring constructs, by adding constructs
4865N/Afor choosing the logic and translating specifications among
4865N/Alogics. HetCASL is needed when combining specifications written in
4865N/ACASL with specifications written in its sublanguages and
4865N/Aextensions. HetCASL also allows the integration of logics
4865N/Athat are completely different from the CASL logic.
4865N/AThis document provides a detailed definition of the HetCASL syntax
4865N/Aand an informal description of the semantics, building on the existing
4865N/A title = "{OMD}oc - An Open Markup Format for Mathematical
4865N/A author = "Michael Kohlhase",
4865N/A series = "Lecture Notes in Computer Science",
4865N/A author = {Jan Oliver Wallgr\"un and Lutz Frommberger and Frank Dylla and Diedrich Wolter},
4865N/A title = {{SparQ} User Manual V0.6.2},
4865N/A note = {University of Bremen},
4865N/A author = {Simon {Peyton Jones} and Mark Jones and Erik Meijer},
4865N/A title = {Type classes: exploring the design space},
4865N/A booktitle = {Haskell Workshop},
author = {Daan Leijen and Erik Meijer},
title = {Parsec: Direct Style Monadic Parser Combinators for the Real World},
school = {Departement of Computer Science, Universiteit Utrecht},
title = {The {G}lasgow {H}askell compiler},
author = {M. Roggenbach},
title = {{CSP-CASL} - A new integration of process algebra and algebraic specification},
journal = {Theoretical Computer Science},