@Article{Alagi02, author = {Suad Alagi}, title = {Institutions: integrating objects, {XML} and databases}, journal = {Information and Software Technology}, year = {2002}, Volume = 44, Pages = {207-216}, Abstract = {A general model theory based on institutions is proposed as a formal framework for investigating typed object-oriented, XML and other data models equipped with integrity constraints. A major challenge in developing such a unified model theory is in the requirement that it must be able to handle major structural differences between the targeted models as well as the significant differences in the logic bases of their associated constraint languages. A distinctive feature of this model theory is that it is transformation-oriented. It is based on structural transformations within a particular category of models or across different categories with a fundamental requirement that the associated constraints are managed in such a way that the database integrity is preserved. }, keywords = {ModelTheory Morphisms}, } @incollection{ArraisFiadeiro96, author = {M. Arrais and J. L. Fiadeiro}, title = {Unifying theories in different institutions}, PAGES = {81--101}, BOOKTITLE = {Recent Trends in Data Type Specifications. 11th Workshop on Specification of Abstract Data Types}, EDITOR = {M. Haveraaen and O. Owe and O.-J. Dahl}, Publisher = {Springer Verlag}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {1130}, year = 1996, keywords = {Morphisms}, } @INCOLLECTION{AstesianoCerioli92, AUTHOR = "E. Astesiano and M. Cerioli", TITLE = "Relationships between Logical Frameworks", BOOKTITLE = "Proc. 8th ADT workshop", EDITOR = {M. Bidoit and C. Choppy}, SERIES = "Lecture Notes in Computer Science", VOLUME = 655, PAGES = {126--143}, PUBLISHER = {Springer Verlag}, keywords = {Logics Morphisms}, YEAR = 1992 } @incollection{Borzyszkowski99, author = {T. Borzyszkowski}, title = {Moving specification structures between logical systems}, series = "Lecture Notes in Computer Science", editor = "J. L. Fiadeiro", booktitle = {Recent Trends in Algebraic Development Techniques, 13th International Workshop, WADT'98, Lisbon, Portugal, April 1998, Selected Papers}, publisher = "Springer", pages = {16--30}, volume = {1589}, year = "1999", keywords = {Morphisms ProofTheory}, } @PHDTHESIS{Cerioli93, AUTHOR = {M. Cerioli}, TITLE = {Relationships between Logical Formalisms}, SCHOOL = {TD-4/93, Universit\`a di Pisa-Genova-Udine}, YEAR = 1993, keywords = {Logics Morphisms}, } @INCOLLECTION{CerioliMeseguer93, author = "M. Cerioli and J. Meseguer", title = "May {I} Borrow Your Logic?", year = 1993, volume = "711", series = "Lecture Notes in Computer Science", publisher = "Springer Verlag, Berlin", Editor = {A.M. Borzyszkowski and S.Sokolowski}, booktitle = "Proc. MFCS'93 (Mathematical Foundations of Computer Science)", note = {To appear in Theoretical Computer Science}, pages = "342--351", keywords = {Morphisms}, } @Article{CerioliMeseguer97, Author = {Cerioli, M. and Meseguer, J.}, Title = {May {I} Borrow Your Logic? (Transporting Logical Structures along Maps)}, Journal = "Theoretical Computer Science", volume = 173, pages = {311--347}, Year = 1997, keywords = {Morphisms}, } @techreport{DimitrakosBicarreguiMaibaum99, author = "Theodosis Dimitrakos and Juan Bicarregui and T.S.E. Maibaum", title = "Integrating Heterogeneous Formalisms: Framework and Application", note = {Technical Report, Rutherford Appleton Laboratory}, year = 1999, keywords = {Morphisms}, url = "citeseer.nj.nec.com/413478.html" } @unpublished{GoguenRosu01, author = {J. Goguen and G. Rosu}, title = {Institution morphisms}, note = {Formal aspects of computing, to appear}, volume = {13}, year = {2002}, pages = {274-307}, keywords = {Morphisms}, } @article{HarperSannellaTarlecki94, author = {Robert Harper and Donald Sannella and Andrzej Tarlecki}, title = {Structured Presentations and Logic Representations}, journal = {Annals of Pure and Applied Logic}, volume = 67, pages = {113--160}, year = 1994, url = {ftp://ftp.dcs.ed.ac.uk/pub/dts/apal.ps}, postscript = {apal.ps}, abstract = {The purpose of a logical framework such as LF is to provide a language for defining logical systems suitable for use in a logic-independent proof development environment. All inferential activity in an object logic (in particular, proof search) is to be conducted in the logical framework via the representation of that logic in the framework. An important tool for controlling search in an object logic, the need for which is motivated by the difficulty of reasoning about large and complex systems, is the use of structured theory presentations. In this paper a rudimentary language of structured theory presentations is presented, and the use of this structure in proof search for an arbitrary object logic is explored. The behaviour of structured theory presentations under representation in a logical framework is studied, focusing on the problem of ``lifting'' presentations from the object logic to the metalogic of the framework. The topic of imposing structure on logic presentations, so that logical systems may themselves be defined in a modular fashion, is also briefly considered.}, comment = {Reviewed in MR~95i:03024; this is the extended final version of SannellaDT:structure-representation89/89a}, keywords = {Morphisms}, } @ARTICLE{KreowskiMossakowski95, TITLE = {Equivalence and Difference of Institutions: Simulating Horn Clause Logic With Based Algebras}, AUTHOR = {H.-J. Kreowski and T. Mossakowski}, JOURNAL = { Mathematical Structures in Computer Science}, VOLUME = {5}, YEAR = 1995, pages = {189--215}, keywords = {Morphisms}, } @INCOLLECTION{MartiOlietMeseguer95, AUTHOR = {N. Mart\'{\i}-Oliet and J. Meseguer}, TITLE = {From Abstract Data Types to Logical Frameworks}, YEAR = 1995, keywords = {Metaformalisms Morphisms}, editor = {Egidio Astesiano and Gianna Reggio and Andrzej Tarlecki}, title = {Recent Trends in Data Type Specification, 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, S. Margherita, Italy, May 30 - June 3, 1994, Selected Papers}, series = {Lecture Notes in Computer Science}, volume = 906, publisher = {Springer}, pages = {48--80}, } @Article{MartiniWolter98, author = "A. Martini and U. Wolter", title = "A systematic study of mappings between institutions", journal = "Lecture Notes in Computer Science", volume = "1376", pages = "300--315", year = "1998", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Sat Oct 10 14:40:24 MDT 1998", acknowledgement =ack-nhfb, keywords = {Morphisms}, } @Article{MartiniWolter99, author = "Alfio Martini and Uwe Wolter", title = "A Single Perspective on Arrows between Institutions", journal = "Lecture Notes in Computer Science", volume = "1548", pages = "486--501", year = "1999", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Tue Feb 5 11:53:33 MST 2002", url = "http://link.springer-ny.com/link/service/series/0558/bibs/1548/15480486.htm; http://link.springer-ny.com/link/service/series/0558/papers/1548/15480486.pdf", acknowledgement =ack-nhfb, keywords = {Morphisms}, } @INCOLLECTION{Meseguer89, AUTHOR = "J. Meseguer", TITLE = "General Logics", BOOKTITLE = "Logic Colloquium 87", PAGES = {275--329}, PUBLISHER = "North Holland", YEAR = 1989, keywords = {Metaformalisms Morphisms}, } @article{Meseguer92, AUTHOR = {J.~Meseguer}, TITLE = {Conditional Rewriting as a Unified Model of Concurrency}, JOURNAL = {Theoretical Computer Science}, VOLUME = {96}, NUMBER = {1}, PAGES = {73--156}, YEAR = {1992}, keywords = {Logics Morphisms}, } @incollection{Meseguer98, author = {J. Meseguer}, title = {Membership Algebra as a Logical Framework for Equational Specification}, booktitle = {Recent trends in algebraic development techniques. Proc.\ 12th International Workshop}, editor = {F. {Parisi Presicce}}, series = {Lecture Notes in Computer Science}, volume = {1376}, pages = {18--61}, publisher = {Springer}, year = {1998}, keywords = {Morphisms}, } @article{Mossakowski02, author = {Till Mossakowski}, title = {Relating {\CASL} with Other Specification Languages: the Institution Level}, year = 2002, volume = {286}, pages = {367--475}, journal = {Theoretical Computer Science}, keywords = {Morphisms}, } @INCOLLECTION{Mossakowski95, AUTHOR = "T. Mossakowski", TITLE = {Equivalences among various logical frameworks of partial algebras}, BOOKTITLE = {Computer Science Logic. 9th Workshop, CSL'95. Paderborn, Germany, September 1995, Selected Papers}, EDITOR = {H. Kleine B\"uning}, SERIES = {Lecture Notes in Computer Science}, VOLUME = 1092, PUBLISHER = {Springer Verlag}, PAGES = {403--433}, YEAR = 1996, keywords = {Morphisms}, } @INCOLLECTION{Mossakowski96b, AUTHOR = "T. Mossakowski", TITLE = {Different Types of Arrow Between Logical Frameworks}, BOOKTITLE = {Proc. ICALP 96}, editor = {F. Meyer auf der Heide and B. Monien}, series = {Lecture Notes in Computer Science}, volume = 1099, Publisher = {Springer Verlag}, pages = {158--169}, year = 1996, keywords = {Morphisms}, } @phdthesis{Mossakowski96c, AUTHOR = "T. Mossakowski", title = {Representations, hierarchies and graphs of institutions}, school = {Bremen University}, note = {Revised version: Logos Verlag, 2001}, year = 1996, keywords = {Logics Morphisms}, } @INCOLLECTION{Mossakowski99, author = "T. Mossakowski", title = "Translating {OBJ3} to {\CASL}: the institution level", series = "Lecture Notes in Computer Science", editor = "J. L. Fiadeiro", booktitle = {Recent Trends in Algebraic Development Techniques, 13th International Workshop, WADT'98, Lisbon, Portugal, April 1998, Selected Papers}, volume = {1589}, pages = {198--214}, publisher = "Springer-Verlag", year = "1999", keywords = {Morphisms}, } @INCOLLECTION{SalibraScollo92, AUTHOR = "A. Salibra and G. Scollo", TITLE = "A soft stairway to institutions", BOOKTITLE = "Proc. 8th ADT workshop", EDITOR = {M. Bidoit and C. Choppy}, SERIES = "Lecture Notes in Computer Science", VOLUME = 655, PAGES = {310--329}, PUBLISHER = {Springer Verlag}, YEAR = 1992, keywords = {Metaformalisms Morphisms}, } @InCollection{SalibraScollo93b, author = {A. Salibra and G. Scollo}, title = {Compactness and L\"{o}wenheim-Skolem properties in pre-institution categories}, booktitle = {Algebraic Methods in Logic and in Computer Science}, keywords = {Morphisms Metatheorems}, pages = {67--94}, year = {1993}, editor = {C.Rauszer}, volume = {28}, series = {Banach Center Publications}, } @Article{SalibraScollo96, title = "Interpolation and compactness in categories of pre-institutions", author = "Antonino Salibra and Giuseppe Scollo", pages = "261--286", journal = "Mathematical Structures in Computer Science", month = jun, year = "1996", volume = "6", number = "3", references = "\cite{JACM::GoguenB1992} \cite{TCS::MancaSS1990} \cite{IC::SannellaT1988} \cite{TCS::Tarlecki1985}", keywords = {Morphisms Metatheorems}, } @inbook{SannellaTarlecki-ch10, Author = {D. Sannella and A. Tarlecki}, Title = {Working with multiple logical systems, In: Foundations of Algebraic Specifications and Formal Program Development}, publisher = {Cambridge University Press, to appear}, note = {See \verb|http://zls.mimuw.edu.pl/~tarlecki/book/index.html|}, chapter = 10, keywords = {Morphisms}, } @phdthesis{Scollo93, author = {G. Scollo}, title = {On the engineering of logics}, year = {1993}, note = {University of Twente, Enschede}, keywords = {Metaformalisms Morphisms}, } @UNPUBLISHED{Tarlecki87, AUTHOR = {A. Tarlecki}, TITLE = {Institution representation}, NOTE = {draft note}, YEAR = 1987, keywords = {Morphisms}, } @incollection{Tarlecki96a, Author = {A. Tarlecki}, Title = {Moving between logical systems}, BOOKTITLE = {Recent Trends in Data Type Specifications. 11th Workshop on Specification of Abstract Data Types}, EDITOR = {M. Haveraaen and O. Owe and O.-J. Dahl}, Publisher = {Springer Verlag}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {1130}, PAGES = {478--502}, year = 1996, keywords = {Morphisms Combination}, } @misc{Tarlecki97, author = "Andrzej Tarlecki", title = "Limits and colimits in some categories of institutions", keywords = {Metatheorems Morphisms Combination}, abstract = {This paper presents a number of concepts of a mapping between logical systems modelled as institutions, discusses their mutual merits and demerits, and sketches their role in the process of system specification and development. Some simple properties of the resulting categories of institutions are given. 1 Introduction We have to live with a multitude of logical systems used in various approaches to software specification and development. The proliferation of logical systems in the area is not just researchers' fancy, but results from the very practical needs to capture various aspects of software systems and to cater for various programming paradigms. Each of them leads to a different... }, url = "citeseer.nj.nec.com/tarlecki97limit.html", } @InCollection{WolterEtal95, key = "Wolter, {\em et al.}", author = "U. Wolter and K. Didrich and F. Cornelius and M. Klar and R. Wess{\"a}ly and H. Ehrig", title = "How to cope with the Spectrum of {\sc Spectrum}", pages = "173--189", annote = "17 references.", editor = "Manfred Broy and Stefan J{\"a}hnichen", booktitle = "{KORSO}: Methods, Languages and Tools for the Construction of Correct Software", publisher = "Springer-Verlag", address = "New York, NY", series = "Lecture Notes in Computer Science", volume = "1009", year = "1995", keywords = {Logics Morphisms}, abstract = {The specification language SPECTRUM [BFG+ 93] melts a wide range of concepts into a single language frame: three-valued first-order logic, polymorphism, type classes, higher-order functions, infinite objects. The desire of identifying and relating sub-languages satisfying certain constraints given by syntactical and pragmatic considerations appears. In this paper we consider the constructive oriented algebraic sub-language ACT ONE as an example of a specification sub-language of SPECTRUM. As a candidate for an implementation language of SPECTRUM we focus on the functional language OPAL. The overall intention is to establish a semantically compatible embedding of ACT ONE and OPAL into SPECTRUM. However, in this paper we will not describe all aspects of this embedding. As a first step of our ongoing work we will relate the underlying logical systems using the concept of institutions, i.e. we will relate the loose semantics of ACT ONE and OPAL specifications with the loose semantics of SPECTRUM specifications. A general framework for modelling the interconnections of different logical systems under development at the TU Berlin will be sketched. }, } @InProceedings{Scollo02, author = "G. Scollo", title = "Graph colouring institutions (Extended Abstract)", editor = "M. Wirsing and D. Pattinson and R. Hennicker", booktitle = "WADT 2002, 16th International Workshop on Algebraic Development Techniques", location = "Frauenchiemsee, Germany", month = sep, year = "2002", pages = "21--22", howpublished = "Technical Report 0207, Institut f\"{u}r Informatik, LMU M\"{u}nchen", note = "This paper proposes an institution design problem, which is solved in \cite{Scollo03a}, as well the problem of designing an isomorphism between the subject institutions, that is solved in \cite{Scollo03b}. ", keywords = {Logics Morphisms}, abstract = {Maximal planar graphs with vertex resp.\ edge colouring are naturally casted as (deceiptively similar) institutions. One then tries to embody Tait's equivalence algorithms into morphisms between them, and is lead to a partial redesign of those institutions. This paper aims at elucidating the pragmatic questions which arise in this case study. }, } @InProceedings{Scollo03a, author = "G. Scollo", title = "Graph colouring institutions", editor = "R. Berghammer and B. M\"{o}ller", booktitle = "7th Seminar RelMiCS and 2nd Workshop Kleene Algebra", location = "Bad Malente, Germany", month = may, year = "2003", pages = "288--297", howpublished = "Christian-Albrechts-Universit\"{a}t zu Kiel", ps = "http://www.informatik.uni-kiel.de/~relmics7/submitted/Scollo/GCI03.ps", pdf = "http://www.informatik.uni-kiel.de/~relmics7/submitted/Scollo/GCI03.pdf", note = "This paper solves the institution design problem proposed in \cite{Scollo02}, but leaves open the isomorphism design problem, which is solved in \cite{Scollo03b}. ", keywords = {Logics Morphisms}, abstract = {Maximal planar graphs with vertex resp.\ edge colouring are naturally casted as (deceiptively similar) institutions. One then tries to embody Tait's equivalence algorithms into morphisms between them, and is lead to a partial redesign of those institutions. This paper aims at introducing a few pragmatic questions which arise in this case study, which also showcases the use of relational concepts and notations in the design of the subject institutions. }, } @misc{Scollo03b, author = "G. Scollo", title = "An institution isomorphism for planar graph colouring", institution = "Universit\`{a} di Verona, Dip.\ Informatica", type = "Draft", year = "2003", month = jun, note = "Submitted for publication. This paper is a revised and extended version of \cite{Scollo03a}, and contains a concise outline of a solution to the isomorphism design problem proposed there. The detailed solution is available in \cite{Scollo03c}. ", keywords = {Logics Morphisms}, abstract = {Maximal planar graphs with vertex resp.\ edge colouring are naturally casted as (deceiptively similar) institutions. One then tries to embody Tait's equivalence algorithms into morphisms between them, and is lead to a partial redesign of those institutions. This paper aims at introducing a few pragmatic questions which arise in this case study, which also showcases the use of relational concepts and notations in the design of the subject institutions, and gives an outline of a solution to the problem of designing an isomorphism between them. }, } @TechReport{Scollo03c, author = "G. Scollo", title = "Morphism-driven design of graph colouring institutions", institution = "Universit\`{a} di Verona, Dip.\ Informatica", type = "Research Report", number = "DI RR 03/2003", year = "2003", month = mar, pdf = "http://www.di.univr.it/~scollo/papers/dirr0303.pdf", note = "Submitted for publication. This paper solves the isomorphism design problem posed in \cite{Scollo02,Scollo03a}, giving the details of the solution outlined in \cite{Scollo03b}. ", keywords = {Logics Morphisms}, abstract = {Maximal planar graphs with vertex resp.\ edge colouring are naturally casted as (deceiptively similar) institutions. One then tries to embody Tait's equivalence algorithms into morphisms between them, and is lead to a partial redesign of those institutions. This paper aims at elucidating the pragmatic questions which arise in this case study, which also showcases the use of relational concepts and notations in the design of the subject institutions, that is driven by the design of an isomorphism between them. }, }