@InProceedings{AgustiCullellEtAl91, author = "J. Agust{\'i}-Cullell and F. Esteva and P. Garcia and L. Godo", title = "Formalizing Multiple-Valued Logics as Institutions", pages = "269--278", ISBN = "3-540-54346-5", editor = "Bernadette Bouchon-Meunier and Ronald R. Yager and Lotfi A. Zadeh", booktitle = "Proceedings of Uncertainty in Knowledge Bases ({IPMU} '90)", month = jul, series = "LNCS", volume = "521", publisher = "Springer", address = "Berlin, Germany", year = "1991", keywords = {Logics}, } @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}, } @article{Aspinall95, author = "D. Aspinall", title = "Types, Subtypes, and {ASL+}", journal = "Lecture Notes in Computer Science", volume = "906", pages = "116--??", year = "1995", keywords = {ModelTheory}, abstract = {ASL+ is a formalism for specification and programming in-the-large, based on an arbitrary institution. It has rules for proving the satisfaction and refinement of specifications, which can be seen as a type theory with subtyping, including contravariant refinement for \Pi-abstracted specifications and a notion of stratified equality for higher-order objects. We describe the syntax of the language and a partial equivalence relation semantics. This style of semantics is familiar from subtyping calculi, but a novelty here is the use of a hierarchy of typed domains instead of a single untyped domain. }, url = "citeseer.nj.nec.com/aspinall95types.html" } @PhdThesis{Aspinall97, author = {David Aspinall}, title = {Type Systems for Modular Programming and Specification}, school = {Edinburgh}, year = {1997}, keywords = {ModelTheory}, } @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{AstesianoCerioli94, Author = {Astesiano, E. and Cerioli, M.}, Title = {Multiparadigm Specification Languages: a First Attempt at Foundations}, booktitle = {Semantics of Specification Languages (SoSl 93)}, editor = {C.M.D.J. Andrews and J.F. Groote}, series = {Workshops in Computing}, publisher = {Springer Verlag}, pages = {168--185}, year = 1994, keywords = {Heterogeneity}, } @Article{Barwise74, title = "Axioms for Abstract Model Theory", author = "Jon Barwise", journal = "Annals of Mathematical Logic", volume = "7", pages = "221--265", year = "1974", keywords = {Metaformalisms}, } @INCOLLECTION{Baumeister91, AUTHOR = "H. Baumeister", TITLE = "Unifying Initial and Loose Semantics of Parameterized Specifications in an Arbitrary Institution", BOOKTITLE = "TAPSOFT 91 Vol. 1: CAAP 91", EDITOR = {S. Abramsky and T.S.E. Maibaum}, SERIES = "Lecture Notes in Computer Science", VOLUME = 493, PAGES = {103--120}, PUBLISHER = {Springer Verlag}, YEAR = 1991, keywords = {ModelTheory}, } @Incollection{Baumeister95, author = "H. Baumeister", title = "Relations as Abstract Datatypes: An Institution to Specify Relations Between Algebras", Publisher = {Springer Verlag}, editor = {Peter D. Mosses and Mogens Nielsen and Michael I. Schwartzbach}, booktitle = {TAPSOFT'95: Theory and Practice of Software Development, 6th International Joint Conference}, series = {Lecture Notes in Computer Science}, volume = "915", pages = "756--771", year = "1995", coden = "LNCSD9", ISSN = "0302-9743", keywords = {ModelTheory}, } @phdthesis{Baumeister98, author = "H. Baumeister", title = "Relations between Abstract Datatypes modeled as Abstract Datatypes", school = "Universit{\"a}t des Saarlandes", year = "1998", keywords = {ModelTheory}, } @InCollection{Baumeister99, author = "Hubert Baumeister", title = "Relating Abstract Datatypes and Z-Schemata", editor = "Didier Bert and Christine Choppy", booktitle = "Recent Trends in Algebraic Development Techniques - Selected Papers", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", volume = "1827", pages = "366--382", year = "2000", keywords = {Logics}, } @InProceedings{BeierlelncsVoss87, author = "C. Beierle and A. Voss", title = "Viewing Implementations as an Institution", pages = "196--218", ISBN = "3-540-18508-9", editor = "D. E. Rydeheard {D.H. Pitt, A. Poign{\'e}}", booktitle = "Proceedings of the Conference on Category Theory and Computer Science", address = "Edinburgh, UK", month = sep, year = "1987", series = "LNCS", volume = "283", publisher = "Springer", keywords = {ModelTheory}, } @Article{BernotBidoitKnapik95, author = {Gilles Bernot and Michel Bidoit and Teodor Knapik}, title = {Observational specifications and the indistinguishability assumption}, journal = {Theoretical Computer Science}, year = {1995}, keywords = {Logics}, volume = {139}, pages = {275--314}, abstract = {To establish the correctness of some software w.r.t. its formal specification is widely recognized as a difficult task. A first simplification is obtained when the semantics of an algebraic specification is defined as the class of all algebras which correspond to the correct realizations of the specification. A software is then declared correct if some algebra of this class corresponds to it. We approach this goal by defining an observational satisfaction relation which is less restrictive than the usual satisfaction relation. Based on this notion we provide an institution for observational specifications. The idea is that the validity of an equational axiom should depend on an observational equality, instead of the usual equality. We show that it is not reasonable to expect an observational equality to be a congruence. We define an observational algebra as an algebra equipped with an observational equality which is an equivalence relation but not necessarily a congruence. We assume that two values can be declared indistinguishable when it is impossible to establish they are different using some available observations. This is what we call the Indistinguishability Assumption . Since term observation seems sufficient for data type specifications, we define an indistinguishability relation on the carriers of an algebra w.r.t. the observation of an arbitrary set of terms. From a careful case study it follows that this requires to take into account the continuations of suspended evaluations of observation terms. Since our indistinguishability relation is not transitive, it is only an intermediate step to define an observational equality. Our approach is motivated by several examples. }, } @incollection{BernotCoudertLeGall96, author = "G. Bernot and S. Coudert and P. {Le Gall}", title = "Towards Heterogeneous Formal Specifications", series = "Lecture Notes in Computer Science", booktitle = "AMAST 96", volume = "1101", pages = "458--472", year = "1996", keywords = {Heterogeneity}, } @misc{BicarreguiDimitrakos00, author = "Juan Bicarregui and Theo Dimitrakos", title = "Interpolation in practical formal development", booktitle = {FAPR2000, International Conference on Pure and Applied Practical Reasoning, London}, year = 2000, keywords = {ProofTheory}, url = "citeseer.nj.nec.com/293777.html" } @incollection{BidoitCengarleHennicker99, author = "Michel Bidoit and Mar\'{\i}a Victoria Cengarle and Rolf Hennicker", title = "Proof systems for structured specifications and their refinements", booktitle = "Algebraic Foundations of Systems Specification", publisher = "Springer", editor = "Egidio Astesiano and Hans-J{\"o}rg Kreowski and Bernd Krieg-Br{\"u}ckner", pages = "385--433", year = "1999", keywords = {ProofTheory}, abstract = {Introduction Reasoning about speci cations is one of the fundamental activities in the process of formal program development. This ranges from proving the consequences of a speci cation, during the prototyping or testing phase for a requirements speci cation, to proving the correctness of re nements (or implementations) of speci cations. The main proof techniques for algebraic speci- cations have their origin in equational Horn logic and term rewriting. These proof methods have been well studied in the case of nonstructured speci cations (see Chapters 9 and 10). For large systems of speci cations built using the structuring operators of speci cation languages, relatively few proof...}, url = "citeseer.nj.nec.com/bidoit99proof.html", } @misc{BidoitHennicker, author = "Michel Bidoit and Rolf Hennicker", title = "On Observability and Reachability", url = "citeseer.nj.nec.com/500492.html", keywords = {Logics}, abstract = {Observability and reachability are important concepts in formal software development. While observability concepts allow to specify the required observable behavior of a program or system, reachability concepts are used to describe the underlying data in terms of data type constructors. In this paper we show that there is a duality between observability and reachability, both from a methodological and from a formal point of view. In particular, we establish a correspondence between observer operations and data type constructors, observational algebras and constructor-based algebras, and observational and inductive properties of specifications. Our study is based on the...}, } @incollection{BidoitHennicker02, author = {Michel Bidoit and Rolf Hennicker}, title = {On the Integration of Observability and Reachability Concepts}, pages = {21--36}, editor = {Mogens Nielsen and Uffe Engberg}, booktitle = {Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {2303}, year = {2002}, isbn = {3-540-43366-X}, keywords = {Logics}, url = "http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/rr-lsv-2002-2.rr.ps", otherurl = "citeseer.nj.nec.com/bidoit02integration.html", abstract = "This paper focuses on the integration of reachability and observability concepts within an algebraic, institution-based framework. We develop the essential notions that are needed to construct an institution which takes into account both the generation- and observation-oriented aspects of software systems. Thereby the underlying paradigm is that the semantics of a specification should be as loose as possible to capture all its correct realizations. We also consider the so-called ``idealized models'' of a specification which are useful to study the behavioral properties a user can observe when he/she is experimenting with the system. Finally, we present sound and complete proof systems that allow us to derive behavioral properties from the axioms of a given specification.", } @inproceedings{BidoitHennicker93, author = "Michel Bidoit and Rolf Hennicker", title = "A General Framework for Modular Implementations of Modular System Specifications", booktitle = "{TAPSOFT}", pages = "199-214", year = "1993", keywords = {ModelTheory}, abstract = {We investigate the impact of modularity on the semantics and on the implementation of software specifications. Based on the stratified loose semantics approach we develop a suitable specification framework which meets our basic requirements: the independent construction of implementations for the single constituent parts (modules) of a system specification and the encapsulated development of each implementation part using the principle of stepwise refinement. Our paper is not aimed at providing an elaborated specification language but rather to concentrate on the modularity issues of system development. Hence, only few but powerful constructs are provided which can be seen as a kernel for ...}, url = "citeseer.nj.nec.com/bidoit93general.html", } @inproceedings{BidoitHennickerKurz01, author = "Michel Bidoit and Rolf Hennicker and Alexander Kurz", title = "On the Duality between Observability and Reachability", booktitle = "Foundations of Software Science and Computation Structure", pages = "72-87", year = "2001", url = "http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/rr-lsv-2001-7.rr.ps", otherurl = "citeseer.nj.nec.com/bidoit01duality.html", keywords = {Logics}, abstract = "Observability and reachability are important concepts in formal software development. While observability concepts allow to specify the required observable behavior of a program or system, reachability concepts are used to describe the underlying data in terms of datatype constructors. In this paper, we show that there is a duality between observability and reachability, both from a methodological and from a formal point of view. In particular, we establish a correspondence between observer operations and datatype constructors, observational algebras and constructor-based algebras, and observational and inductive properties of specifications. Our study is based on the observational logic institution~\cite{hb:ol} and on a novel treatment of reachability which introduces the constructor-based logic institution. Both institutions are tailored to capture the semantically correct realizations of a specification from the observational and reachability points of view. The duality between the observability and reachability concepts is then formalized in a category-theoretic setting.", } @article{BidoitSannellaTarlecki02, author = {Michel Bidoit and Donald Sannella and Andrzej Tarlecki}, title = {Architectural Specifications in {CASL}}, journal = {Formal Aspects of Computing}, year = {2002}, volume = 13, pages = {252--273}, url = {ftp://ftp.dcs.ed.ac.uk/pub/dts/archs.ps}, dvi = {archs.dvi}, postscript = {archs.ps}, pdf = {archs.pdf}, abstract = {One of the most novel features of CASL, the Common Algebraic Specification Language, is the provision of so-called architectural specifications for describing the modular structure of software systems. A brief discussion of refinement of CASL specifications provides the setting for a presentation of the rationale behind architectural specifications. This is followed by some details of the features provided in CASL for architectural specifications, hints concerning their semantics, and simple results justifying their usefulness in the development process.}, note = {This is an extended version of SannellaDT:arch-specs98 that supercedes Report ECS-LFCS-99-407, Laboratory for Foundations of Computer Science, Univ.\ of Edinburgh (1999)} } @Article{BidoitTarlecki96, author = "M. Bidoit and A. Tarlecki", title = "Behavioural Satisfaction and Equivalence in Concrete Model Categories", journal = "Lecture Notes in Computer Science", volume = "1059", pages = "241--256", year = "1996", ISSN = "0302-9743", keywords = {Metaformalisms}, abstract = {We use the well-known framework of concrete categories to show how much of standard universal algebra may be done in an abstract and still rather intuitive way. This is used to recast the unifying view of behavioural semantics of speci cations based on behavioural satisfaction and, respectively, on behavioural equivalence of models abstracting away from many particular features of standard algebras. We also give an explicit representation of behavioural equivalence between models in terms of behavioural correspondences.}, } @ARTICLE{BlackburnRijke97, author = "P. Blackburn and M. de Rijke", title = "Why combine logics?", journal = "Studia Logica", year = 1997, volume = 59, pages = {5--27}, keywords = {Combination}, } @Incollection{Borzyszkowski98, author = "T. Borzyszkowski", title = "Correctness of a logical system for structured specifications", booktitle = {Recent trends in algebraic development techniques. Proc.\ 12th International Workshop}, editor = {F. {Parisi Presicce}}, series = {Lecture Notes in Computer Science}, volume = "1376", pages = "107--121", year = "1998", coden = "LNCSD9", ISSN = "0302-9743", keywords = {ProofTheory}, } @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}, } @inproceedings{Borzyszkowski00, author = "Tomasz Borzyszkowski", title = "Higher-Order Logic and Theorem Proving for Structured Specifications", booktitle = "Workshop on Algebraic Development Techniques 1999", pages = "401-418", year = "2000", editor = "Christine Choppy and Didier Bert and Peter Mosses", series = "LNCS", volume = "1827", keywords = {Logics}, } @article{Borzyszkowski02, author = {T.~Borzyszkowski}, title = {Logical systems for structured specifications}, journal = {Theoretical Computer Science}, volume = {286}, year = 2002, pages = {197-245}, keywords = {ProofTheory}, } @inbook{BurstallDiaconescu94, AUTHOR = {R. Burstall and R. Diaconescu}, TITLE = {Hiding and behaviour: an institutional approach}, BOOKTITLE = {A Classical Mind: Essays Dedicated to C.A.R. Hoare}, editor = {A. William Roscoe}, pages = {75--92}, PUBLISHER = {Prentice-Hall}, keywords = {ModelTheory}, YEAR = {1994} } @TechReport{CaleiroEtAl00, address = "1049-001 Lisboa, Portugal", author = "C. Caleiro and W. A. Carnielli and M. E. Coniglio and A. Sernadas and C. Sernadas", institution = "Section of Computer Science, Department of Mathematics, Instituto Superior T\'ecnico", note = "Submitted for publication", title = "Fibring non-truth-functional logics: Completeness preservation", type = "Preprint", year = "2000", ps = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/00-CCCSS-fiblog8.ps", pdf = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/00-CCCSS-fiblog8.pdf", st = "s", proj = "fiblog", keywords = {Combination}, } @incollection{CaleiroEtAl01, title = {Combining Logics: Parchments Revisited}, author = {C.Caleiro and P.Mateus and J.Ramos and A.Sernadas}, Editor = {M. Cerioli and G. Reggio}, Booktitle = {Recent Trends in Algebraic Development Techniques, 15th International Workshop, WADT'01, Genova, Italy}, series = "Lecture Notes in Computer Science", publisher = "Springer-Verlag", pages = {48--70}, volume = 2267, keywords = {Combination}, } @InCollection{CaleiroSernadasSernadas99a, author = "C. Caleiro and C. Sernadas and A. Sernadas", title = "Parameterisation of Logics", editor = "J. Fiadeiro", booktitle = "Recent Trends in Algebraic Development Techniques - Selected Papers", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", volume = "1589", pages = "48--62", year = "1999", ps = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/98-CSS-paramlog.ps", st = "p", proj = "fiblog,acl,logcomp", keywords = {Combination}, } @TechReport{CaleiroSernadasSernadas99b, author = "C. Caleiro and C. Sernadas and A. Sernadas", title = "Mechanisms for combining logics", type = "Research Report", institution = "Section of Computer Science, Department of Mathematics, Instituto Superior T\'ecnico", address = "1049-001 Lisboa, Portugal", year = "1999", ps = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/99-CSS-comblog.ps", st = "i", proj = "fiblog,acl,logcomp", keywords = {Combination}, } @Article{CazuanescuRosu97, title = "Weak inclusion systems", author = "Virgil Emil C{\u{a}}z{\u{a}}nescu and Grigore Ro{\c{s}}u", pages = "195--206", journal = "Mathematical Structures in Computer Science", month = apr, year = "1997", volume = "7", number = "2", references = "\cite{JACM::GoguenB1992} \cite{TCS::Tarlecki1985}", keywords = {Metaformalisms}, } @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}, } @InProceedings(CerioliReggio93, Author = {Cerioli, M. and Reggio, G.}, Title = {Algebraic-Oriented Institutions}, BookTitle = {Algebraic Methodology and Software Technology (AMAST'93)}, Publisher = {Springer}, Editor = {Nivat, M. and Rattray, C. and Rus, T. and Scollo, G.}, Series = {Workshops in Computing}, Pages = "103--210", pages = {Metaformalisms}, Year = 1994 ) @Article{CerioliReggio94, author = "M. Cerioli and G. Reggio", title = "Institutions for very abstract specifications", journal = "Lecture Notes in Computer Science", volume = "785", pages = "113--127", year = "1994", coden = "LNCSD9", ISSN = "0302-9743", keywords = {Combination}, } @Incollection{CerioliZucca97, author = {M. Cerioli and E. Zucca}, title = {Implementation of Derived Programs (Almost) for Free}, booktitle = {Recent trends in algebraic development techniques. Proc.\ 12th International Workshop}, editor = {F. {Parisi Presicce}}, series = {Lecture Notes in Computer Science}, volume = {1376}, publisher = {Springer}, Year = 1998, pages = {141--155}, keywords = {ModelTheory Metaformalisms}, } @InCollection{Cirstea02, author = {Corina Cirstea}, title = {Institutionalising Many-Sorted Coalgebraic Modal Logic}, booktitle = {CMCS 2002}, publisher = {Elsevier Science}, year = {2002}, series = {Electronic Notes in Theoretical Computer Science}, keywords = {Logics}, } @article{ClassenGrosse-RhodeWolter95, author = {Cla{\ss}en, I. and Gro{\ss}e--Rhode, M. and Wolter, U.}, title = {Categorical Concepts for Parameterized Partial Specifications}, journal = {Math. Struct. in Comp. Science}, year = {1995}, volume = {5}, pages = {153--188}, keywords = {Logics}, note = {A preliminary version appeared as Tech. Report 92-42, Technische Universit{\"a}t Berlin, FB Informatik, 1992} } @TechReport{ConiglioEtAl00, author = "M. E. Coniglio and A. T. Martins and A. Sernadas and C. Sernadas", title = "Fibring (Para)consistent Logics", type = "Research Report", institution = "Section of Computer Science, Department of Mathematics, Instituto Superior T\'ecnico", address = "1049-001 Lisboa, Portugal", year = "2000", note = "Extended abstract. Presented at II World Congress on Paraconsistency - WCP'00", ps = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/00-CMSS-fiblog6.ps", pdf = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/00-CMSS-fiblog6.pdf", st = "c", proj = "fiblog,logcomp", keywords = {Combination}, } @TechReport{ConiglioSernadasSernadas02, author = "M. E. Coniglio and A. Sernadas and C. Sernadas", institution = "Section of Computer Science, Department of Mathematics, Instituto Superior T\'ecnico", address = "1049-001 Lisboa, Portugal", note = "Submitted for publication", title = "Topos-theoretic semantics of fibring", type = "Preprint", year = "2002", ps = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/02-CSS-fiblog14.ps", pdf = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/02-CSS-fiblog14.pdf", st = "s", proj = "fiblog", keywords = {Combination}, } @article{CorneliusEtAl95, author = {Cornelius, F. and Ehrig, H. and Orejas, F. and Baldamus, M.}, title = {Abstract and behaviour module specifications}, journal = {Mathematical Structures in Computer Science}, volume = 9, pages = {21--62}, year = {1999}, abstract = {The theory of algebraic module specifications and modular systems developed mainly in the framework of equational algebraic specifications is shown to be almost independent of the und erlying kind of specifications. In fact, it is shown in this paper that the theory can be formulated entirely on the level of specification frames using indexed categories. In this framework it is called abstract module specifications. Main results concerning correctness and compositionality of abstract module specifications can be obtained if the category of abstract specifications has certain kinds of pushouts which allow amalgamations and/or extensions on the semantical level, as well as suitable free constructions. The theory of abstract module specifications is applied to the behaviour specification frame in the sense of Nivela and Orejas leading to behaviour module specifications.}, keywords = {ModelTheory}, } @Incollection{CostaLourenco01, author = "J. F{\'e}lix Costa and H. Louren{\c{c}}o", title = "Canonical Institutions of Behaviour", Editor = {M. Cerioli and G. Reggio}, Booktitle = {Recent Trends in Algebraic Development Techniques, 15th International Workshop, WADT'01, Genova, Italy}, series = "Lecture Notes in Computer Science", publisher = "Springer-Verlag", year = {2002}, volume = "2267", pages = "71--84", year = "2001", ISSN = "0302-9743", url = "http://link.springer-ny.com/link/service/series/0558/bibs/2267/22670071.htm; http://link.springer-ny.com/link/service/series/0558/papers/2267/22670071.pdf", keywords = {Logics}, } @incollection{CoudertBernotLeGall99, author = "S. Coudert and G. Bernot and P. {Le Gall}", title = "Hierarchical Heterogeneous Specifications", 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 = {106--120}, volume = {1589}, year = "1999", keywords = {Heterogeneity}, } @article{Diaconescu00, author = "Razvan Diaconescu", title = "Category-based constraint logic", journal = "Mathematical Structures in Computer Science", volume = "10", number = "3", pages = "373-407", year = "2000", keywords = {ModelTheory Logics}, url = "citeseer.nj.nec.com/diaconescu99categorybased.html", } @article{Diaconescu01, author = {R. Diaconescu}, title = {Grothendieck institutions}, journal = {Applied categorical structures}, volume = {10}, year = {2002}, pages = {383--402}, keywords = {Heterogeneity}, } @misc{Diaconescu94, author = "R. Diaconescu", title = "Category-based Semantics for Equational and Constraint Logic Programming", text = "Razvan Diaconescu. Category-based Semantics for Equational and Constraint Logic Programming. PhD thesis, University of Oxford, 1994.", year = "1994", keywords = {Metaformalisms Logics}, url = "citeseer.nj.nec.com/diaconescu94categorybased.html" } @inproceedings{Diaconescu95a, author = "Razvan Diaconescu", title = "A Category-Based Equational Logic Semantics to Constraint Programming", 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}, VOLUME = {1130}, series = {Lecture Notes in Computer Science}, year = 1996, pages = "200-221", keywords = {Metaformalisms Logics}, url = "citeseer.nj.nec.com/article/diaconescu96categorybased.html" } @article{Diaconescu95b, author = "Razvan Diaconescu", title = "Completeness of Category-Based Equational Deduction", journal = "Mathematical Structures in Computer Science", volume = "5", number = "1", pages = "9-40", year = "1995", keywords = {Metaformalisms Logics}, url = "citeseer.nj.nec.com/315755.html" } @article{Diaconescu96, author = "R\u{a}zvan Diaconescu", title = "Category-Based Modularisation for Equational Logic Programming", journal = "Acta Informatica", volume = "33", pages = "477--510", year = "1996", keywords = {Metaformalisms Logics}, url = "citeseer.nj.nec.com/diaconescu96categorybased.html" } @article{Diaconescu97, AUTHOR = {R. Diaconescu}, TITLE = {Extra Theory Morphisms for Institutions: logical semantics for multi-paradigm languages}, pages = {427--453}, volume = {6}, journal = {J. Applied Categorical Structures}, year = 1998, keywords = {Heterogeneity}, } @article{DiaconescuFutatsugi02, author = "R. Diaconescu and K. Futatsugi", title = "Logical foundations of {CafeOBJ}", journal = {Theoretical computer science}, volume = {285}, pages = {289--318}, year = {2002}, keywords = {ModelTheory Logics Heterogeneity}, } @INPROCEEDINGS{DiaconescuGoGuenStefaneas91, AUTHOR = {Diaconescu, R{\u{a}}zvan and Goguen, Joseph and Stefaneas, Petros}, TITLE = {Logical Support for Modularisation}, BOOKTITLE = {Proceedings of a Workshop on Logical Frameworks}, EDITOR = {Huet, Gerard and Plotkin, Gordon}, YEAR = {1991}, HOWPUBLISHED = {Programming Research Group, Oxford University}, keywords = {ModelTheory}, } @misc{Dimitrakos97, author = "T. Dimitrakos", title = "Modularity and interpolation in a development workspace", text = "T. Dimitrakos. Modularity and interpolation in a development workspace. Technical report, Imperial College, 1997.", year = "1997", keywords = {ProofTheory}, url = "citeseer.nj.nec.com/dimitrakos97modularity.html" } @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" } @article{DimitrakosMaibaum00, author = "Theodosis Dimitrakos and Tom Maibaum", title = "On a generalised modularisation theorem", journal = "Information Processing Letters", volume = "74", number = "1-2", pages = "65--71", year = "2000", keywords = {ProofTheory}, url = "citeseer.nj.nec.com/dimitrakos00generalised.html" } @techreport{DimitrakosMaibauma, author = "T. Dimitrakos and T.S.E. Maibaum", title = "Development Workspaces: an introduction", keywords = {ProofTheory}, url = "citeseer.nj.nec.com/417497.html" } @inbook{DimitrakosMaibaumb, author = "T. Dimitrakos and T.S.E. Maibaum", title = "Notes on Refinement, Interpolation and Uniformity.", pages = {108-116}, year = {1997}, booktitle = {International Conference on Automated Software Engineering (ASE '97), November 2-5}, keywords = {ProofTheory}, url = "citeseer.nj.nec.com/410195.html" } @techreport{DimitrakosMaibaumc, author = "Theodosis Dimitrakos and Tom Maibaum ", title = "Hiding information via abstraction", keywords = {ProofTheory}, url = "citeseer.nj.nec.com/411997.html" } @techreport{Diskin94, author = {Z. Diskin}, title = {Algebraizing Institutions: Incorporating Algebraic Logic Methodology into the institution Framework for Builing Specifications}, institution = {Laboratory for Database Design, Riga, Latvija}, year = 1994, keywords = {Metaformalisms}, } @Incollection{DocheWiels00, author = "Marielle Doche and Virginie Wiels", title = "Extended Institutions for Testing", journal = "Lecture Notes in Computer Science", volume = "1816", editor = {Teodor Rus}, booktitle = {Algebraic Methodology and Software Technology. 8th International Conference, AMAST 2000}, pages = "514--528", year = "2000", ISSN = "0302-9743", url = "http://link.springer-ny.com/link/service/series/0558/bibs/1816/18160514.htm; http://link.springer-ny.com/link/service/series/0558/papers/1816/18160514.pdf", keywords = {Metaformalisms}, } @incollection{DuranMeseguer99, author = "Francisco Dur\'an and Jos\'e Meseguer", title = "Structured Theories and Institutions", editor = {Martin Hofmann and Giuseppe Rosolini and Dusko Pavlovic}, booktitle = {CTCS '99 Conference on Category Theory and Computer Science}, series = {Electronic Notes in Theoretical Computer Science}, volume = 29, year = 1999, keywords = {ModelTheory}, url = "citeseer.nj.nec.com/465777.html" } @book{EhrichGogollaLipeck89, author = {Ehrich, H.-D. and Gogolla, M. and Lipeck, U.W.}, title = {Algebraische Spezifikation abstrakter Datentypen}, publisher = {Teubner, Stuttgart}, year = 1989, keywords = {Metaformalisms Logics} } @TechReport{EhrigBaldamusCornelius91, title = "Abstract Module Specifications in the Framework of Specification Logics and Applications to Behavioural Module Specifications", author = "Harmut Ehrig and Michael Baldamus and Felix Cornelius and Fernando Orejas", year = "1991", key = {ModelTheory}, institution = "Technical University of Berlin", } @InProceedings{EhrigBaldamusOrejas92, author = "H.~Ehrig and M.~Baldamus and F.~Orejas", title = "New {C}oncepts of {A}malgamation and {E}xtension for a {G}eneral {T}heory of Specifications", booktitle = "Recent Trends in Data Type Specification, Proceedings ADT--COMPASS--Workshop Durdan'91", year = "1992", pages = "199--221", SERIES = {Lecture Notes in Computer Science}, PUBLISHER = {Springer}, key = {ModelTheory}, volume = "655" , } @InProceedings{EhrigEtAl95, author = "Hartmut Ehrig and Martin Grosse-Rhode and Uwe Wolter", title = "On the Role of Category Theory in the Area of Algebraic Specifications", editor = "M. Haveraaen and O. Owe and O. J. Dahl", booktitle = "Recent Trends in Data Type Specification", series = "Lecture Notes in Computer Science", publisher = "Springer-Verlag", year = "1995", pages = "17--48", volume = "1130", keywords = {Categories}, abstract = {Paradigm and main concepts of category theory in view of application in theoretical computer science are summarized. In more detail we present three selected problems in the area of algebraic specifications concerning a unified framework for specification logics, partial algebras, and models for cncurrent systems, which are solved using concepts, constructions and results of category theory. In order to solve two of the problems we point out the idea of classifying categories, that allows to present categories of algebras as functor categories and to derive a number of important results in a unified way. }, } @ARTICLE{EhrigGrosseRhode94, AUTHOR = "H. Ehrig and M. Gro\ss{}e--{R}hode", TITLE = "Functorial theory of parameterized specifications in a general specification framework", JOURNAL = "Theoretical Computer Science", VOLUME = 135, PAGES = {221--266}, YEAR = 1994, abstract = {A general specification framework based on the notion of indexed categories is introduced in order to study the structural aspects of specifications independent of the underlying logics. Similar to institutions this concept of specification frames allows to formulate a unified structural theory of various kinds of algebraic specifications which have been studied separately in the literature before. In contrast to institutions we do not require to have satisfaction relations and conditions which allows to handle also behavioural specifications and semantics and various concepts of constraints in this framework. In this framework we generalize the well-known theory of parameterized algebraic specifications with initial semantics from the equational case to specification frames satisfying mainly three basic axioms. The existence of pushouts, free constructions and amalgamation. Moreover, an axiomatic treatment of restriction is presented which allows to study in addition to refinement also implementations of parameterized specifications including restrictions. Finally we present an axiomatic framework for functorial semantics which opens the way to apply the theory not only to initial semantics but also to other kinds of functorial semantics, including final and specific kinds of loose semantics. }, keywords = {ModelTheory}, } @INCOLLECTION{EhrigJimenezOrejas93, AUTHOR = {H. Ehrig and R. M. Jimenez and F. Orejas}, TITLE = {Compositionality Results for Different Types of Parameterization and Parameter Passing in Specification Languages}, BOOKTITLE = {TAPSOFT 93}, EDITOR = {M.-C. Gaudel and J.-P. Jouannaud}, SERIES = {Lecture Notes in Computer Science}, PUBLISHER = {Springer Verlag}, VOLUME = 668, PAGES = {31--45}, YEAR = 1993, keywords = {ModelTheory}, } @InProceedings{EhrigJimenezOrejas93, author = "H.~Ehrig and A.M.~Jimenez and F.~Orejas", title = "Compositionality {R}esults for {D}ifferent {T}ypes of {P}arametrization and {P}arameter {P}assing in {S}pecification {L}anguages", booktitle = "Proc. TAPSOFT'93", year = "1993", volume = "668", SERIES = {Lecture Notes in Computer Science}, PUBLISHER = {Springer Verlag}, pages = "31--45", month = "April", key = {ModelTheory}, } @incollection{EhrigKreowski99, AUTHOR = {H. Ehrig and H.-J. Kreowski}, TITLE = {Refinement and Implementation}, BOOKTITLE = {Algebraic Foundations of Systems Specifications}, PUBLISHER = {Springer Verlag}, pages = {201--242}, keywords = {ModelTheory}, EDITOR = {E.~Astesiano and H.-J.~Kreowski and B.~Krieg--Br\"uckner}, YEAR = {1999}, } @BOOK{EhrigMahr90, AUTHOR = "H. Ehrig and B. Mahr", TITLE = "Fundamentals of Algebraic Specification 2", PUBLISHER = "Springer Verlag, Heidelberg", YEAR = 1990, keywords = {ModelTheory}, } @incollection{Fiadeiro96, author = "J. L. Fiadeiro", title = "On the Emergence of Properties in Component-Based Systems", booktitle = "Algebraic Methodology and Software Technology. Proceedings - 1996", volume = "1101", series = {Lecture Notes in Computer Science}, publisher = "Springer-Verlag", address = "Berlin, Germany", editor = "M. Wirsing and M. Nivat", pages = "421--443", year = "1996", keywords = {Logics}, abstract = {When several components are interconnected to form a complex system, they may exhibit more properties (individually) than they had when considered in isolation. When we consider a category SPEC of component specifications taken as theories in some logic, properties are expressed as sentences of the underlying logic, and emergence of properties can be characterised by the fact that the morphisms that connect component specifications to the system specification are not conservative. Depending on the relationship that can be established between SPEC and a corresponding category PROG of programs, we show that such emergence phenomena can be interpreted in more than one way: (1)...}, url = "citeseer.nj.nec.com/fiadeiro96emergence.html" } @InProceedings{FiadeiroCosta94, author = "J. L. Fiadeiro and J. F. Costa", title = "Institutions for Behaviour Specification", editor = "E. Astesiano and G. Reggio and A. Tarlecki", booktitle = "Recent Trends in Data Type Specification", series = "Lecture Notes in Computer Science", publisher = "Springer-Verlag", year = "1994", pages = "273--289", annote = "incomplete", keywords = {Logics}, } @article{FiadeiroCosta96, author = "Jose Luiz Fiadeiro and Jose Felix Costa", title = "Mirror, Mirror in my Hand: A Duality between Specifications and Models of Process Behaviour", journal = "Mathematical Structures in Computer Science", volume = "6", number = "4", pages = "353-373", year = "1996", keywords = {Logics}, abstract = {Since Pnueli's seminal paper in 1977, Temporal Logic has been used as a formalism for specifying and verifying the correctness of reactive systems. In this paper, we show that, besides its expressive power, Temporal Logic enjoys a very strong structural property: it is categorical on processes. That is, we show how temporal specifications (as theories) can be embedded in categories of process behaviour, and out of this adjunction we build an institution which is categorical in the sense of Meseguer. This characterisation means that temporal logic is, in a sense, "sound and complete" with respect to process specification and interconnection techniques.}, url = "citeseer.nj.nec.com/fiadeiro96mirror.html" } @misc{FiadeiroLopesMaibaum97, author = "J. Fiadeiro and A. Lopes and T. Maibaum", title = "Synthesising Interconnections", pages = {240--264}, editor = {Richard S. Bird and Lambert G. L. T. Meertens}, title = {Algorithmic Languages and Calculi, IFIP TC2 WG2.1 International Workshop on Algorithmic Languages and Calculi, 17-22 February 1997, Alsace, France}, booktitle = {Algorithmic Languages and Calculi}, publisher = {Chapman {\&} Hall}, series = {IFIP Conference Proceedings}, volume = {95}, year = {1997}, isbn = {0-412-82050-1}, keywords = {Logics}, abstract = {In the context of the modular and incremental development of complex systems, viewed as interconnections of interacting components, new dimensions and new problems arise in the calculation of programs from specifications. A particularly important aspect for extending existing methods to address composite systems is the ability, given programs that realise component specifications, to synthesise the interconnections between them in such a way that the system specification is realised. Taking our cue from earlier work on General Systems Theory (Goguen, 1973) and more recent work on parallel program design (Fiadeiro and Maibaum, 1996), we discuss, characterise and provide solutions for the... }, url = "citeseer.nj.nec.com/272104.html" } @INCOLLECTION{FiadeiroSernadas88, AUTHOR = {J. Fiadeiro and A. Sernadas}, TITLE = {Structuring theories on consequence}, EDITOR = {D.~Sannella and A.~Tarlecki}, BOOKTITLE = {Recent Trends in Data Type Specification, 5th Workshop on Specification of Abstract Data Types}, SERIES = {Lecture Notes in Computer Science}, PUBLISHER = {Springer Verlag}, PAGES = {44--72}, VOLUME = 332, YEAR = 1988, keywords = {Metaformalisms}, } @ARTICLE{Gabbay95, author = "D. Gabbay", title = "Fibred semantics and the weaving of logics: part 1", journal = "Journal of Symbolic Logic", volume = 61, number = 4, year = 1996, pages = "1057--1120", keywords = {Combination}, } @INCOLLECTION{Gabbay96, author = "D. Gabbay", title = "An overview of fibred semantics and the combination of logics", booktitle = "Frontiers of Combining Systems", editor = "F. Baader and K. Schulz", publisher = "Kluwer Academic Publishers", year = 1996, pages = "1--55", keywords = {Combination}, } @InProceedings{Goguen86, author = "J. A. Goguen", title = "One, none, a hundred thousand specification languages", booktitle = "Information Processing 86", publisher = "North Holland", editor = "H.-J. Kugler", pages = "995--1003", annote = "Report bei Loeckx", year = "1986", } @InCollection{Goguen89a, author = "J. A. Goguen", title = "{Principles of Parameterized Programming}", editor = "T. J. Biggerstaff and C. Richter", booktitle = "{Software Reusability}", publisher = "acm press", year = "1989", volume = "I --- Concepts and Models", publisher = "acm press", year = "1989", chapter = "7", key = {ModelTheory}, pages = "159--225", } @InProceedings{Goguen91a, author = "Joseph A. Goguen", title = "Types as Theories", booktitle = "Proc. of Symposium on General Topology and Applications", publisher = "Oxford University Press", year = "1991", keywords = {ModelTheory}, } @article{Goguen91b, author = "Joseph A. Goguen", title = "A Categorical Manifesto", journal = "Mathematical Structures in Computer Science", volume = "1", number = "1", pages = "49-67", year = "1991", keywords = {Categories}, url = "citeseer.nj.nec.com/goguen91categorical.html" } @article{Goguen92, author = "Joseph A. Goguen", title = "Sheaf Semantics for Concurrent Interacting Objects", journal = "Mathematical Structures in Computer Science", volume = "2", number = "2", pages = "159--191", year = "1992", url = "citeseer.nj.nec.com/goguen92sheaf.html", abstract = {This paper uses concepts from sheaf theory to explicate phenomena in concurrent systems, including object, inheritance, deadlock, and non-interference, as used in computer security. The approach is very general, and applies not only to concurrent object oriented systems, but also to systems of differential equations, electrical circuits, hardware description languges, and much more. Time can be discrete or continuous, linear or branching, and distribution is allowed over space as well as time. Concepts from category theory help to achieve this generality: objects are modeled by sheaves; inheritance by sheaf morphisms; systems by diagrams; and interconnections by diagrams of diagrams.}, keywords = {Metaformalisms}, } @InProceedings{Goguen96, author = "J. Goguen", title = "Parameterized Programming and Software Architecture", editor = "Murali Sitaraman", booktitle = "Proceedings of the Fourth International Conference on Software Reuse", year = "1996", publisher = "IEEE Computer Society Press", pages = "2--11", referencedby = "\cite{1997:icse:karhinen}, \cite{1997:ssr:karhinen}", key = {ModelTheory}, annote = "incomplete", } @ARTICLE{GoguenBurstall84a, AUTHOR = "J. A. Goguen and R. M. Burstall", TITLE = "Some Fundamentals Algebraic Tools for the Semantics of Computation. {P}art 1: Comma Categories, Colimits, Signatures and Theories", JOURNAL = "Theoretical Computer Science", VOLUME = 31, PAGES = {175--209}, YEAR = 1984, keywords = {Metaformalisms}, } @ARTICLE{GoguenBurstall84b, AUTHOR = "J. A. Goguen and R. M. Burstall", TITLE = "Some Fundamentals Algebraic Tools for the Semantics of Computation. {P}art 2: Signed and Abstract Theories", JOURNAL = "Theoretical Computer Science", VOLUME = 31, PAGES = {263--295}, YEAR = 1984, keywords = {Categories}, } @INCOLLECTION{GoguenBurstall85, AUTHOR = "J. A. Goguen and R. M. Burstall", EDITOR = {D. Pitt et al.}, TITLE = "A Study in the Foundations of Programming Methodology: Specifications, Institutions, Charters and Parchments", BOOKTITLE = {Category Theory and Computer Programming}, SERIES = "Lecture Notes in Computer Science", PUBLISHER = {Springer Verlag}, VOLUME = 240, PAGES = {313-333}, YEAR = 1985, keywords = {Metaformalisms}, } @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, keywords = {Metaformalisms}, } @incollection{GoguenDiaconescu94, author = "J. A. Goguen and R. Diaconescu", title = "Towards an Algebraic Semantics for the Object Paradigm", booktitle = "{RECENT} trends in data type specification: workshop on specification of abstract data types: {COMPASS}: selected papers", number = "785", publisher = "Springer Verlag", address = "Berlin, Germany", year = "1994", keywords = {Logics}, url = "citeseer.nj.nec.com/318274.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}, } @InCollection{GoguenTracz00, key = "Goguen \& Tracz", author = "Joseph A. Goguen and Will Tracz", title = "An Implementation-Oriented Semantics for Module Composition", booktitle = "Foundations of Component-Based Systems", editor = "Gary T. Leavens and Murali Sitaraman", year = "2000", publisher = "Cambridge University Press", address = "New York, NY", ISBN = "0-521-77164-1", chapter = "11", pages = "231--263", annote = "29 references.", url = "citeseer.nj.nec.com/206136.html", keywords = {ModelTheory}, } @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}, } @unpublished{Hilberdink95, author = {H. Hilberdink}, title = {The End of Syntax. {T}he End of Algebra}, note = {Manuscripts, St. Peter's College, Oxford}, YEAR = 1995, keywords = {Metaformalisms}, } @Article{JimenezOrejasEhrig95, author = {R. M. Jimenez and F. Orejas and H. Ehrig}, title = {Compositionality and compatibility of parameterization and parameter passing in specification languages}, journal = {MSCS}, year = {1995}, keywords = {ModelTheory}, volume = {5}, number = {2}, pages = {283--314}, abstract = {In this paper we continue previous work by Sannella, Sokolowski and Tarlecki on parameterization in specification languages. Within the loose approach, we define specification and model level semantics for two kinds of parameterizations (parameterized specifications and specifications of parameterized data types) and describe, in a compositional manner, parameter passing at both levels. Moreover, the specification and the model level semantics of parameter passing are shown to be compatible. We also show that the results obtained do not only apply to the loose approach but can also be directly applicable to the initial framework, and in general to any other kind of monomorphic framework (i.e., a framework where all specifications are monomorphic). In particular, the results obtained generalize and extend previous results for the initial approach. Finally, to obtain our results, new categorical constructions of multiple pushouts, amalgamations and extensions, which generalize standard notions of pushouts, amalgamations and extensions, had to be introduced. }, } @inproceedings{KahrsSannellaTarlecki94, author = {Stefan Kahrs and Donald Sannella and Andrzej Tarlecki}, title = {Interfaces and {E}xtended {ML}}, booktitle = {Proc.\ {ACM} Workshop on Interface Definition Languages}, location = {Portland}, pages = {111--118}, publisher = {{ACM} {SIGPLAN} Notices 29(8)}, year = 1994, url = {ftp://ftp.dcs.ed.ac.uk/pub/dts/interfaces.ps}, postscript = {interfaces.ps}, abstract = {This is a position paper giving our views on the uses and makeup of module interfaces. The position espoused is inspired by our work on the Extended ML (EML) formal software development framework and by ideas in the algebraic foundations of specification and formal development. The present state of interfaces in EML is outlined and set in the context of plans for a more general EML-like framework with axioms in interfaces taken from an arbitrary logical system formulated as an \emph{institution}. Some more speculative plans are sketched concerning the simultaneous use of multiple institutions in specification and development.}, keywords = {Heterogeneity}, } @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{Kurz02, author = {Alexander Kurz}, title = {Logics Admitting Final Semantics}, pages = {238--249}, editor = {Mogens Nielsen and Uffe Engberg}, booktitle = {Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {2303}, year = {2002}, isbn = {3-540-43366-X}, keywords = {Metatheorems}, } @inproceedings{LopesFiadeiro97, author = "Antonia Lopes and Jose Luiz Fiadeiro", title = "Preservation and Reflection in Specification", booktitle = "Algebraic Methodology and Software Technology", pages = "380-394", year = "1997", keywords = {Logics}, abstract = {We extend the traditional notion of specification based on theories and interpretations between theories to model situations, typical of open, reactive systems, in which properties exhibited locally by an object no longer hold when that object is interconnected as a component of a larger system. The proposed notion of specification is based on the observation, due to Winskel, that while some assertions are preserved across morphisms of labelled transition systems, other are reflected. The distinction between these two classes of assertions leads us to the definition of two categories of specifications, one that supports horizontal structuring and another that supports vertical...}, url = "citeseer.nj.nec.com/lopes97preservation.html" } @InCollection{LourenSernadas99b, author = "H. {Louren{\c c}o} and A. Sernadas", title = "An Institution of Hybrid Systems", editor = "Didier Bert and Christine Choppy", booktitle = "Recent Trends in Algebraic Development Techniques - Selected Papers", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", volume = "1827", pages = "219--236", year = "2000", ps = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/99-LS-hybint.ps", st = "p", proj = "problog,acl,logcomp", keywords = {Logics}, } @Article{LucioOrejasPino99, author = {Paqui Lucio and Fernando Orejas and Elvira Pino}, title = {An algebraic framework for the definition of compositional semantics of normal logic programs}, journal = {The Journal of Logic Programming}, year = {1999}, key = {ModelTheory Logics}, volume = {40}, number = {1}, pages = {89-123}, abstract = {The aim of our work is the definition of compositional semantics for modular units over the class of normal logic programs. In this sense, we propose a declarative semantics for normal logic programs in terms of model classes that is monotonic in the sense that Mod(P \cup P') \subseteq Mod(P), for any programs P and P', and we show that in the model class associated to every program there is a least model that can be seen as the semantics of the program, which may be built upwards as the least fix point of a continuous immediate consequence operator. In addition, it is proved that this least model is "typical" for the class of models of Clark-Kunen's completion of the program. This means that our semantics is equivalent to Clark-Kunen's completion. Moreover, following the approach defined in a previous paper, it is shown that our semantics constitutes a "specification frame" equipped with the adequate categorical constructions needed to define compositional and fully abstract (categorical) semantics for a number of program units. In particular, we provide a categorical semantics of arbitrary normal logic program fragments which is compositional and fully abstract with respect to the (standard) union. }, } @TechReport{MaibaumFiadeiroSadler90, key = "Maibaum \& Fiadeiro \& Sadler", author = "T. Maibaum and J. Fiadeiro and M. Sadler", title = "Stepwise program development in $\pi$-institutions", institution = "Imperial College of Science, Technology and Medicine, Department of Computing", year = "1990", keywords = {ProofTheory}, } @INCOLLECTION{MartiOlietMeseguer94, AUTHOR = {N. Mart\'{\i}-Oliet and J. Meseguer}, TITLE = {General Logics and Logical Frameworks}, BOOKTITLE = {What is a Logical System?}, EDITOR = {D. M. Gabbay}, PUBLISHER = {Oxford University Press}, YEAR = 1994, keywords = {Metaformalisms}, } @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}, } @TECHREPORT{Mayoh85, AUTHOR = {B. Mayoh}, TITLE = {Galleries and institutions}, TYPE = {Report {DAIMI} {PB}-191}, INSTITUTION = {Aarhus University}, YEAR = 1985, keywords = {Metaformalisms}, } @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}, } @incollection{Mossakowski00c, Author = {T. Mossakowski}, Title = {Specification in an arbitrary institution with symbols}, Editor = {C. Choppy and D. Bert and P. Mosses}, Booktitle = {Recent Trends in Algebraic Development Techniques, 14th International Workshop, WADT'99, Bonas, France}, series = "Lecture Notes in Computer Science", publisher = "Springer-Verlag", volume = {1827}, year = 2000, pages = {252--270}, keywords = {Metaformalisms ModelTheory}, } @incollection{Mossakowski01, Author = {T. Mossakowski}, Title = {Heterogeneous development graphs and heterogeneous borrowing}, Booktitle = {Foundations of Software Science and Computation Structures}, Editor = {M. Nielsen and U. Engberg}, series = "Lecture Notes in Computer Science", publisher = "Springer-Verlag", volume = {2303}, pages = {326--341}, year = {2002}, keywords = {Heterogeneity}, } @unpublished{Mossakowski02b, Author = {T. Mossakowski}, Title = {Comorphism-based Grothendieck logics}, Note = {Submitted}, keywords = {Heterogeneity}, } @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{Mossakowski94, AUTHOR = "T. Mossakowski", TITLE = {A Hierarchy of Institutions separated by properties of parameterized abstract data types}, EDITOR = {E. Astesiano and G. Reggio and A. Tarlecki}, BOOKTITLE = {Recent Trends in Data Type Specification. Proceedings}, SERIES = {Lecture Notes in Computer Science}, PUBLISHER = {Springer Verlag, London}, VOLUME = 906, PAGES = {389--405}, YEAR = 1995, keywords = {Metatheorems}, } @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{Mossakowski96a, AUTHOR = "T. Mossakowski", TITLE = "Using limits of parchments to systematically construct institutions of partial algebras", 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}, VOLUME = {1130}, series = {Lecture Notes in Computer Science}, PAGES = {379--393}, year = 1996, keywords = {Combination}, } @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{MossakowskiEtAl00, Author = {T. Mossakowski and S. Autexier and D. Hutter}, Title = {Extending Development Graphs With Hiding}, Editor = {H. Hu\ss{}mann}, Booktitle = {Fundamental Approaches to Software Engineering}, Year = {2001}, series = "Lecture Notes in Computer Science", publisher = "Springer-Verlag", volume = {2029}, pages = {269--283}, keywords = {ProofTheory}, } @incollection{MossakowskiKlin01, Author = {T. Mossakowski and B. Klin}, Title = {Institution Independent Static Analysis for {\CASL}}, Editor = {M. Cerioli and G. Reggio}, Booktitle = {Recent Trends in Algebraic Development Techniques, 15th International Workshop, WADT'01, Genova, Italy}, series = "Lecture Notes in Computer Science", publisher = "Springer-Verlag", year = {2002}, pages = {221--237}, volume = {2267}, keywords = {ProofTheory}, } @INCOLLECTION{MossakowskiTarleckiPawlowski97a, Author = {T. Mossakowski and A. Tarlecki and W. Paw\l{}owski}, Title = {Combining and Representing Logical Systems}, BOOKTITLE = {Category Theory and Computer Science, 7th Int. Conf.}, EDITOR = {E. Moggi and G. Rosolini}, SERIES = {Lecture Notes in Computer Science}, PUBLISHER = {Springer Verlag}, VOLUME = 1290, pages = {177--196}, YEAR = 1997, keywords = {Combination}, } @INCOLLECTION(MossakowskiTarleckiPawlowski97b, Author = {T. Mossakowski and A. Tarlecki and W. Paw\l{}owski}, Title = {Combining and Representing Logical Systems Using Model-Theoretic Parchments}, booktitle = {Recent trends in algebraic development techniques. Proc.\ 12th International Workshop}, editor = {F. {Parisi Presicce}}, series = {Lecture Notes in Computer Science}, volume = {1376}, pages = {349--364}, publisher = {Springer}, year = {1998}, keywords = {Combination}, ) @INCOLLECTION{Mosses89, AUTHOR = {P. D. Mosses}, TITLE = {Unified Algebras and Institutions}, SERIES = {Proceedings of the 4th Annual IEEE Symposium on Logic in Computer Science}, PAGES = {304--312}, YEAR = 1989, keywords = {Logics}, } @Misc{NielsenPletat86, title = "Polymorphism in an Institutional Framework", author = "Mogens Nielsen and Udo Pletat", year = "1986", note = "Technical University of Denmark", keywords = {Logics}, } @incollection{Orejas99, AUTHOR = {F. Orejas}, TITLE = {Structuring and Modularity}, BOOKTITLE = {Algebraic Foundations of Systems Specifications}, PUBLISHER = {Springer Verlag}, pages = {159--200}, keywords = {ModelTheory}, EDITOR = {E.~Astesiano and H.-J.~Kreowski and B.~Krieg--Br\"uckner}, YEAR = {1999}, } @Article{OrejasPinoEhrig97, title = "Institutions for logic programming", author = "Fernando Orejas and Elvira Pino and Hartmut Ehrig", pages = "485--511", journal = "Theoretical Computer Science", month = "28~" # feb, year = "1997", volume = "173", number = "2", preliminary = "mfcs::OrejasPE1994", references = "\cite{TCS::FalaschiLPM1989} \cite{POPL::GaifmanS1989} \cite{LICS::GaifmanS1989} \cite{JACM::goguenB1992} \cite{POPL::JaffarL1987} \cite{JLOGP::Miller1989} \cite{LICS::Stuckey1991}", key = {ModelTheory Logics}, abstract = {The compositionality of the semantics of logic programs with respect to (different varieties of) program union has been studied recently by a number of researchers. The approaches used can be considered quite ad hoc in the sense that they provide, from scratch, the semantic constructions needed to ensure compositionality and, in some cases, full abstraction in the given framework. In this paper, we study the application of general algebraic methods for obtaining, systematically, this kind of results. In particular, the method proposed consists in studying the adequate institution for describing the given class of logic programs and, then, in using general institution-independent results to prove compositionality and full abstraction. This is done in detail for the class of definite logic programs with respect to three kinds of composition operations: \Omega-union, standard union and module composition. In addition two different institutions are considered: the standard institution of Horn clause logic and a new institution that better captures the input/output operational behaviour of logic programs. Finally, a similar solution is sketched for other classes of logic programs. }, } @Article{Pawlowski01, author = "Wies{\l}aw Paw{\l}owski", title = "Presentations for Abstract Context Institutions", journal = "Lecture Notes in Computer Science", volume = "2267", pages = "256--279", year = "2001", ISSN = "0302-9743", url = "http://link.springer-ny.com/link/service/series/0558/bibs/2267/22670256.htm; http://link.springer-ny.com/link/service/series/0558/papers/2267/22670256.pdf", keywords = {Metaformalisms}, } @incollection{Pawlowski95a, author = {W. Paw{\l}owski}, title = {Context Institutions}, 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 = {436--457}, year = 1996, keywords = {Metaformalisms}, } @incollection(Pawlowski98, author = {W. Paw{\l}owski}, title = {Context Parchments}, booktitle = {Recent trends in algebraic development techniques. Proc.\ 12th International Workshop}, editor = {F. {Parisi Presicce}}, series = {Lecture Notes in Computer Science}, volume = {1376}, pages = {381--401}, publisher = {Springer}, year = {1998}, keywords = {Metaformalisms}, ) @INCOLLECTION{Poigne89, AUTHOR = {A. Poign\'{e}}, TITLE = {Foundations are Rich Institutions, but Institutions are Poor Foundations}, BOOKTITLE = {Categorical Methods in Computer Science, With Aspects from Topology}, EDITOR = {H. Ehrig et al.}, SERIES = {Lecture Notes in Computer Science}, PUBLISHER = {Springer Verlag}, VOLUME = 393, PAGES = {82--101}, YEAR = 1989, keywords = {Metaformalisms}, } @PHDTHESIS{Posegga88, AUTHOR = {Michael Posegga}, TITLE = {Algebraic model theories: a contribution to the generalization of the notion ``logical system''}, SCHOOL = {Humboldt Universit\"at Berlin???}, NOTE = {Report der Akademie der Wissenschaften der DDR, 1988-4}, YEAR = 1988, keywords = {Metaformalisms}, } @Article{RasgaEtAl01, abstract = "We give a categorial characterization of how labelled deduction systems for logics with a propositional basis behave under unconstrained fibring and under fibring that is constrained by symbol sharing. At the semantic level, we introduce a general semantics for our systems and then give a categorial characterization of fibring of models. Based on this, we establish the conditions under which our systems are sound and complete with respect to the general semantics for the corresponding logics, and establish requirements on logics and systems so that completeness is preserved by both forms of fibring.", author = "Jo{\~a}o Rasga and Am{\'\i}lcar Sernadas and Cristina Sernadas and Luca Vigan{\`o}", journal = "Journal of Logic and Computation", language = "USenglish", note = "To appear", title = "Fibring Labelled Deduction Systems", year = "2001", keywords = {Combination}, } @InProceedings{Reggio91, author = "G. Reggio", title = "Entities: An Institution for Dynamic Systems", pages = "246--265", ISBN = "3-540-54496-8", editor = "Hartmut Ehrig and Klaus P. Jantke and Fernando Orejas and Horst Reichel", booktitle = "Proceedings of Recent Trends in Data Type Specification", month = apr, series = "LNCS", volume = "534", publisher = "Springer", address = "Berlin, Germany", year = "1991", pages = "246--265", keywords = {Logics}, } @Article{Rosu94, author = "G. Rosu", title = "The Institution of Order-Sorted Equational Logic", journal = "Bulletin of the European Association for Theoretical Computer Science", volume = "53", pages = "250--255", month = jun, year = "1994", note = "Technical Contributions", keywords = {Logics}, } @Article{Rosu99, author = "G. Rosu", title = "{Kan} Extensions of Institutions", journal = "J.UCS: Journal of Universal Computer Science", volume = "5", number = "8", pages = "482--??", day = "28", month = aug, year = "1999", ISSN = "0948-6968", url = "http://www.jucs.org/jucs_5_8/kan_extensions_of_institutions", acknowledgement =ack-nhfb, keywords = {Metatheorems}, } @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}, } @TechReport{SalibraScollo92, author = "A. Salibra and G. Scollo", title = "Compactness and Loewenheim-Skolem Properties in Categories of Pre-Institutions", address = "Liens", year = "1992", keywords = {Metatheorems}, } @Article{SalibraScollo93a, author = {A. Salibra and G. Scollo}, title = {A reduction scheme by pre-institution transformations, (abstract)}, journal = {Journal of Symbolic Logic}, year = {1993}, key = {Morphisms}, volume = {58}, pages = {1130-1131}, } @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}, } @phdthesis{Sannella82, author = {Donald Sannella}, title = {Semantics, Implementation and Pragmatics of {C}lear, a Program Specification Language}, school = {Department of Computer Science, University of Edinburgh}, year = 1982, abstract = {Specifications are necessary for communicating decisions and intentions and for documenting results at many stages of the program development process. Informal specifications are typically used today, but they are imprecise and often ambiguous. Formal specifications are precise and exact but are more difficult to write and understand. We present work aimed toward enabling the practical use of formal specifications in program development, concentrating on the Clear language for structured algebraic specification. Two different but equivalent denotational semantics for Clear are given. One is a version of a semantics due to Burstall and Goguen with a few corrections, in which the category-theoretic notion of a colimit is used to define Clear's structuring operations independently of the underlying ``institution'' (logical formalism). The other semantics defines the same operations by means of straightforward set-theoretic constructions; it is not institution-independent but it can be modified to handle all institutions of apparent interest. Both versions of the semantics have been implemented. The set-theoretic implementation is by far the more useful of the two, and includes a parser and typechecker. An implementation is useful for detecting syntax and type errors in specifications, and can be used as a front end for systems which manipulate specifications. Several large specifications which have been processed by the set-theoretic implementation are presented. A semi-automatic theorem prover for Clear built on top of the Edinburgh LCF system is described. It takes advantage of the structure of Clear specifications to restrict the available information to that which seems relevant to proving the theorem at hand. If the system is unable to prove a theorem automatically the user can attempt the proof interactively using the high-level primitives and inference rules provided. We lay a theoretical foundation for the use of Clear in systematic program development by investigating a new notion of the implementation of a specification by a lower-level specification. This notion extends to handle parameterised specifications. We show that this implementation relation is transitive and commutes with Clear's structuring operations under certain conditions. This means that a large specification can be refined to a program in a gradual and modular fashion, where the correctness of the individual refinements guarantees the correctness of the resulting program.}, comment = {Report CST-17-82}, keywords = {ModelTheory}, } @article{SannellaSokolowskiTarlecki92, author = {Donald Sannella and Stefan Soko{\l}owski and Andrzej Tarlecki}, title = {Toward Formal Development of Programs from Algebraic Specifications: Parameterisation Revisited}, journal = {Acta Informatica}, volume = 29, number = 8, pages = {689--736}, comment = {Reviewed in CR 9405-0310, CR 9503-0176; an early version of this, with an extended example in an appendix, appeared as report 6/90, Univ. Bremen, 1990}, year = 1992, url = {ftp://ftp.dcs.ed.ac.uk/pub/dts/param.ps}, postscript = {param.ps}, abstract = {Parameterisation is an important mechanism for structuring programs and specifications into modular units. The interplay between parameterisation (of programs and of specifications) and specification (of parameterised and of non-parameterised programs) is analysed, exposing important semantic and methodological differences between specifications of parameterised programs and parameterised specifications. The extension of parameterisation mechanisms to the higher-order case is considered, both for parameterised programs and parameterised specifications, and the methodological consequences of such an extension are explored. A specification formalism with parameterisation of an arbitrary order is presented. Its denotational-style semantics is accompanied by an inference system for proving that an object satisfies a specification. The formalism includes the basic specification-building operations of the ASL specification language and is institution independent.}, keywords = {ModelTheory}, } @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}, } @inproceedings{SannellaTarlecki86, author = {Donald Sannella and Andrzej Tarlecki}, title = {Extended {ML}: An Institution-Independent Framework for Formal Program Development}, booktitle = {Proc.\ Workshop on Category Theory and Computer Programming}, location = {Guildford}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 240, pages = {364--389}, year = 1986, url = {ftp://ftp.dcs.ed.ac.uk/pub/dts/abstract-eml.ps}, postscript = {abstract-eml.ps}, abstract = {The Extended ML specification language provides a framework for the formal stepwise development of modular programs in the Standard ML programming language from specifications. The object of this paper is to equip Extended ML with a semantics which is completely independent of the logical system used to write specifications, building on Goguen and Burstall's work on the notion of an \emph{institution} as a formalisation of the concept of a logical system. One advantage of this is that it permits freedom in the choice of the logic used in writing specifications; an intriguing side-effect is that it enables Extended ML to be used to develop programs in languages other than Standard ML since we view programs as simply Extended ML specifications which happen to include only ``executable'' axioms. The semantics of Extended ML is defined in terms of the primitive specification-building operations of the ASL kernel specification language which itself has an institution-independent semantics. It is not possible to give a semantics for Extended ML in an institutional framework without extending the notion of an institution; the new notion of an \emph{institution with syntax} is introduced to provide an adequate foundation for this enterprise. An institution with syntax is an institution with three additions: the category of signatures is assumed to form a concrete category; an additional functor is provided which gives concrete syntactic representations of sentences; and a natural transformation associates these concrete objects with the ``abstract'' sentences they represent. We use the first addition to ``lift'' certain necessary set-theoretic constructions to the category of signatures, and the other two additions to deal with the low-level semantics of axioms.}, comment = {Reviewed in MR~88f:68100; somewhat obsolete with respect to the current design of Extended ML but the technicalities are still relevant}, keywords = {Metaformalisms}, } @article{SannellaTarlecki87, author = {Donald Sannella and Andrzej Tarlecki}, title = {On Observational Equivalence and Algebraic Specification}, journal = {Journal of Computer and System Sciences}, volume = 34, pages = {150--178}, year = 1987, abstract = {The properties of a simple and natural notion of observational equivalence of algebras and the corresponding specification-building operation are studied. We begin with a definition of observational equivalence which is adequate to handle reachable algebras only, and show how to extend it to cope with unreachable algebras and also how it may be generalised to make sense under an arbitrary institution. Behavioural equivalence is treated as an important special case of observational equivalence, and its central role in program development is shown by means of an example.}, comment = {Reviewed in MR 88j:68118 and CR 8808-0615; this is the final complete version of SannellaDT:observational-equivalence85}, keywords = {ModelTheory}, } @article{SannellaTarlecki88a, author = {Donald Sannella and Andrzej Tarlecki}, title = {Toward Formal Development of Programs from Algebraic Specifications: Implementations Revisited}, journal = {Acta Informatica}, volume = 25, pages = {233--281}, year = 1988, url = {ftp://ftp.dcs.ed.ac.uk/pub/dts/impl.ps}, postscript = {impl.ps}, abstract = {The program development process is viewed as a sequence of implementation steps leading from a specification to a program. Based on an elementary notion of refinement, two notions of implementation are studied: constructor implementations which involve a construction ``on top of'' the implementing specification, and abstractor implementations which additionally provide for abstraction from some details of the implemented specification. These subsume most formal notions of implementation in the literature. Both kinds of implementations satisfy a vertical composition and a (modified) horizontal composition property. All the definitions and results are shown to generalise to the framework of an arbitrary institution, and a way of changing institutions during the implementation process is introduced. All this is illustrated by means of simple concrete examples.}, comment = {This is the final version of SannellaDT:implementations-revisited87}, keywords = {ModelTheory}, } @article{SannellaTarlecki88b, author = {Donald Sannella and Andrzej Tarlecki}, title = {Specifications in an Arbitrary Institution}, journal = {Information and Computation}, volume = 76, pages = {165--210}, year = 1988, abstract = {A formalism for constructing and using axiomatic specifications in an arbitrary logical system is presented. This builds on the framework provided by Goguen and Burstall's work on the notion of an \emph{institution} as a formalisation of the concept of a logical system for writing specifications. We show how to introduce free variables into the sentences of an arbitrary institution and how to add quantifiers which bind them. We use this foundation to define a set of primitive operations for building specifications in an arbitrary institution based loosely on those in the ASL kernel specification language. We examine the set of operations which results when the definitions are instantiated in institutions of total and partial first-order logic and compare these with the operations found in existing specification languages. We present proof rules which allow proofs to be conducted in specifications built using the operations we define. Finally, we introduce a simple mechanism for defining and applying parameterised specifications and briefly discuss the program development process.}, comment = {Reviewed in MR 89d:68056 and Zbl 654.68017; an early short version was SannellaDT:specs-arbitrary-institution84}, keywords = {ModelTheory}, } @Article{Schobbens93, author = {Pierre-Yves Schobbens}, title = {Exceptions for algebraic specifications: on the meaning of "but"}, journal = {Science of Computer Programming}, year = {1993}, key = {Metaformalisms}, volume = {20}, pages = {73--111}, abstract = {When building large specifications from requirements, the structure of the specification becomes a central problem: the specification language should allow a decomposition that closely reflects the structure of requirements. In this paper, we propose a decomposition into defaults (general rules) and exceptions to these general rules that fits the requirements found in some application domains. It is complementary, and builds upon, the modular decomposition proposed by the algebraic specification school. Its definition is based on abstract model theory, leading to the definition of default institutions. }, } @Incollection{SchroederEtAl01a, author = "Lutz Schr{\"o}der and Till Mossakowski and Andrzej Tarlecki and Bartek Klin and Piotr Hoffman", title = "Semantics of Architectural Specifications in {CASL}", Editor = {H. Hu\ss{}mann}, Booktitle = {Fundamental Approaches to Software Engineering}, series = "Lecture Notes in Computer Science", publisher = "Springer-Verlag", volume = "2029", pages = "253--268", year = "2001", ISSN = "0302-9743", url = "http://link.springer-ny.com/link/service/series/0558/bibs/2029/20290253.htm; http://link.springer-ny.com/link/service/series/0558/papers/2029/20290253.pdf", keywords = {ModelTheory}, } @phdthesis{Scollo93, author = {G. Scollo}, title = {On the engineering of logics}, year = {1993}, note = {University of Twente, Enschede}, keywords = {Metaformalisms Morphisms}, } @Article{Sernadas00a, author = "Am\'ilcar Sernadas", title = "Review of {\em Fibring Logics}, by {D}ov {M}. {G}abbay", journal = "Journal of Logic, Language, and Information", year = "2000", volume = "9", number = "4", pages = "511--513", xref = "Review of gabbay:1999a.", topic = "fibred-semantics;modal-logic;", keywords = {Combination}, } @InCollection{SernadasCostaSernadas94, author = "A. Sernadas and J. F. Costa and C. Sernadas", title = "An Institution of Object Behaviour", booktitle = "Recent Trends in Data Type Specification", editor = "H. Ehrig and F. Orejas", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", year = "1994", pages = "337--350", volume = "785", ps = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/94-SCS-iob.ps", st = "p", keywords = {Logics}, } @incollection{SernadasEtAl00, author = {A. Sernadas and C. Sernadas and C. Caleiro and T. Mossakowski}, booktitle = {Frontiers of Combining Systems 2}, editor = {D. Gabbay and Rijke, M. de}, pages = {295--316}, publisher = {Research Studies Press}, title = {Categorical Fibring of Logics with Terms and Binding Operators}, year = {2000}, series = {Studies in Logic and Computation}, keywords = {Combination}, } @InCollection{SernadasSernadas86, author = "C. Sernadas and A. Sernadas", title = "Conceptual Modeling Abstractions as Parameterized Theories in Institutions", booktitle = "Database Semantics, N-H", year = "1986", keywords = {ModelTheory}, } @TechReport{SernadasSernadas93, author = "A. Sernadas and C. Sernadas", title = "Denotational Semantics of Object Specification Within an Arbitrary Temporal Logic Institution", type = "Research Report", institution = "Section of Computer Science, Department of Mathematics, Instituto Superior T\'ecnico", address = "1049-001 Lisboa, Portugal", year = "1993", note = "Presented at IS-CORE Workshop 93", ps = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/93-SS-osli.ps", st = "c", keywords = {Metaformalisms ModelTheory}, } @techreport{SernadasSernadas95, author = {A. Sernadas and C. Sernadas}, title = {Theory Spaces}, type = {Research Report, {DMIST}, 1096 {L}isboa, {P}ortugal}, note = {Presented at ISCORE'95 and ADT/COMPASS'95}, year = 1995, keywords = {Metaformalisms}, } @article{SernadasSernadasCaleiro97a, author = {A. Sernadas and C. Sernadas and C. Caleiro}, title = {Fibring of logics as a categorial construction}, journal = {Journal of Logic and Computation}, volume = {8}, pages = {1--31}, year = {1998}, keywords = {Combination}, } @article{SernadasSernadasCaleiro97b, author = {A. Sernadas and C. Sernadas and C. Caleiro}, title = {Synchronization of Logics}, journal = {Studia Logica}, volume = 59, number = 2, year = 1997, pages = {217-247}, keywords = {Combination}, } @incollection{SernadasSernadasCaleiro97c, author = {A. Sernadas and C. Sernadas and C. Caleiro}, title = {Synchronization of Logics with Mixed Rules: Completeness Preservation}, booktitle = {AMAST97}, publisher = {Springer-Verlag}, year = 1997, volume = "1349", pages = "465--478", series = {Lecture Notes in Computer Science}, volume = {1349}, keywords = {Combination}, } @article{SernadasSernadasCaleiro97d, author = {A. Sernadas and C. Sernadas and C. Caleiro}, title = {Fibring of Logics as a Categorial Construction}, year = 1998, journal = {Journal of Logic and Computation}, volume = 9, pages = {149--179}, year = 1999, keywords = {Combination}, } @InProceedings{SernadasSernadasVelenca94, author = "A. Sernadas and C. Sernadas and J. M. Valenca", title = "A Theory-Based Topological Notion of Institution", editor = "E. Astesiano and G. Reggio and A. Tarlecki", booktitle = "Recent Trends in Data Type Specification", series = "Lecture Notes in Computer Science", publisher = "Springer-Verlag", year = "1994", pages = "420--436", volume = 906, keywords = {Metaformalisms}, } @TechReport{SernadasSernadasZanardo01, author = "A. Sernadas and C. Sernadas and A. Zanardo", institution = "Section of Computer Science, Department of Mathematics, Instituto Superior T\'ecnico", address = "1049-001 Lisboa, Portugal", note = "Submitted for publication", title = "Fibring modal first-order logics: Completeness preservation", type = "Preprint", year = "2001", ps = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/01-SSZ-fiblog4.ps", pdf = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/01-SSZ-fiblog4.pdf", st = "s", proj = "fiblog", keywords = {Combination}, } @techreport{Stefaneas92, author = {P. Stefaneas}, title = {The first order parchment}, institution = {Oxford University Computing Laboratory}, type = {Report {PRG}-{TR}-16-92}, year = 1992, keywords = {Metaformalisms}, } @ARTICLE{Tarlecki85, AUTHOR = "A. Tarlecki", TITLE = "On the Existence of Free Models in Abstract Algebraic Institutions", JOURNAL = "Theoretical Computer Science ", VOLUME = 37, PAGES = {269--304}, YEAR = 1985, keywords = {Metatheorems}, } @ARTICLE{Tarlecki86a, AUTHOR = "A. Tarlecki", TITLE = "Quasi-varieties in Abstract Algebraic Institutions", JOURNAL = "Journal of Computer and System Sciences", VOLUME = 33, PAGES = {333--360}, YEAR = 1986, keywords = {ModelTheory Metatheorems}, } @incollection{Tarlecki86b, Author = {A. Tarlecki}, Title = {Bits and pieces of the theory of institutions}, booktitle = {Proc.\ Intl.\ Workshop on Category Theory and Computer Programming, Guildford 1985}, editor = {D. Pitt and S. Abramsky and A. Poign\'e and D. Rydeheard}, series = {Lecture Notes in Computer Science}, volume = 240, pages = {334--363}, publisher = {Springer-Verlag}, year = 1986, keywords = {Metatheorems Combination}, } @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}, } @techreport{Tarlecki96b, Author = {A. Tarlecki}, Title = {Structural properties of some categories of institutions}, Institution = {Warsaw University}, Year = {1996}, keywords = {Metatheorems}, url = "citeseer.nj.nec.com/tarlecki96structural.html", abstract = {This is a technical paper stating and proving completeness and cocompleteness results for various categories of institutions. 1 Introduction This is a technical companion report to [Tar96], where an overview of various notions of a mapping between institutions is given and some structural properties of the resulting categories of institutions are indicated. The main goal of the current report is to provide technical statements of these results and to prove them in sufficient detail. Some of the results given here have been only hinted at in [Tar96], some of them are repeated from [Tar96], and some are known from the earlier literature. }, } @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", } @InProceedings{Tarlecki98, author = {A. Tarlecki}, title = {Towards Heterogeneous Specifications}, booktitle = {Frontiers of Combining Systems 2, 1998}, editor = {D. Gabbay and Rijke, M. de}, publisher = {Research Studies Press}, year = {2000}, pages = {337--360}, series = {Studies in Logic and Computation}, keywords = {Heterogeneity}, } @incollection{Tarlecki99, AUTHOR = {A. Tarlecki}, TITLE = {Institutions: An abstract framework for formal specifications}, BOOKTITLE = {Algebraic Foundations of Systems Specifications}, PUBLISHER = {Springer Verlag}, pages = {105--130}, EDITOR = {E.~Astesiano and H.-J.~Kreowski and B.~Krieg--Br\"uckner}, keywords = {Metaformalisms}, YEAR = {1999}, } @ARTICLE{TarleckiGoguenBurstall91, AUTHOR = "A. Tarlecki and R. M. Burstall and J. A. Goguen", TITLE = "Some Fundamentals Algebraic Tools for the Semantics of Computation. {P}art 3: Indexed Categories", JOURNAL = "Theoretical Computer Science", VOLUME = 91, PAGES = {239--264}, YEAR = 1991, keywords = {Categories}, } @Article{VelosoFiadeiroVeloso02, author = {Paulo A. S. Veloso and Jos\`e L. Fiadeiro and Sheila R. M. Veloso}, title = {On local modularity and interpolation in entailment systems}, journal = {Information Processing Letters}, year = {2002}, keywords = {ProofTheory}, volume = {82}, number = {4}, pages = {203--211}, abstract = {We generalise and clarify connections between variants of modularity (preservation of faithfulness) and interpolation by localising them to a diagram in an entailment system. The variants of modularity arise naturally from the idea of building specifications in steps. We establish, by an algebraic approach, connections between these variants and (the existence of) versions of interpolating specifications. We also extend these correspondences to specification and interpolating families, and clarify the role of pushout diagrams in this context. }, } @Article{VelosoVeloso01, author = "Paulo A. S. Veloso and Sheila R. M. Veloso", title = "On local modularity variants and {$\Pi$}-institutions", journal = "Information Processing Letters", volume = "77", number = "5--6", pages = "247--253", day = "31", month = mar, year = "2001", coden = "IFPLAT", abstract = {We examine some variants of modularity (preservation of faithfulness) by localizing them to a commutative diagram in a \Pi-institution. We address, by means of an algebraic approach, the question of when a specification is modular for a given pair of specifications. Motivated by design considerations, we extend this notion to families, which leads to simpler variants, with decoupled connections. }, ISSN = "0020-0190", bibdate = "Wed Apr 18 07:11:20 MDT 2001", url = "http://www.elsevier.nl/gej-ng/10/23/20/68/32/28/abstract.html; http://www.elsevier.nl/gej-ng/10/23/20/68/32/28/article.pdf", acknowledgement =ack-nhfb, keywords = {ProofTheory}, } @INCOLLECTION{Wolter95, author = {Wolter, U.}, title = {Institutional Frames}, BOOKTITLE = {Recent Trends in Data Type Specification. Proceedings}, EDTIOR = {E. Astesiano and G. Reggio and A. Tarlecki}, SERIES = {Lecture Notes in Computer Science}, PUBLISHER = {Springer Verlag, London}, VOLUME = 906, year = {1995}, pages = {469--482}, keywords = {Metaformalisms}, } @techreport{WolterEtAl94, author = {Wolter, U. and Klar, M. and Wess{\"a}ly, R. and Cornelius, F.}, title = {{Four Institutions -- A Unified Presentation of Logical Systems for Specification}}, institution = {TU Berlin, Fachbereich Informatik}, year = {1994}, number = {Bericht-Nr. 94-24}, keywords = {Logics}, } @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. }, } @Article{ZanardoSernadasSernadas01, author = "A. Zanardo and A. Sernadas and C. Sernadas", title = "Fibring: Completeness preservation", journal = "Journal of Symbolic Logic", volume = "66", number = "1", pages = "414--439", year = "2001", ps = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/99-ZSS-fiblog3.ps", pdf = "http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/99-ZSS-fiblog3.pdf", st = "p", proj = "fiblog,acl,logcomp", keywords = {Combination}, } @Article{Zucca99, author = {Elena Zucca}, title = {From static to dynamic abstract data-types: an institution transformation}, journal = {Theoretical Computer Science}, year = {1999}, key = {ModelTheory Metaformalisms}, volume = {216}, pages = {109--157}, abstract = {We show how to extend in a canonical way a given formalism for specifying (static) data types (like usual algebraic specification frameworks) with dynamic features. What we obtain in this way is a corresponding formalism for specifying dynamic data-types based on the "state-as-algebra" approach: a dynamic data-type models a dynamically evolving system in which any state can be viewed as a static data type in the underlying formalism, and the dynamic evolution is given by operations handling configurations. Formally, our construction is a functor between two appropriate categories of (specialized) institutions. }, } @misc{ orejas-heterogeneous, author = "Fernando Orejas and Elvira Pino", title = "Heterogeneous Modular Systems", keywords = {Heterogeneity}, url = "citeseer.nj.nec.com/orejas02heterogeneous.html" } @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. }, }