Abstract
We investigate functorial relationships between the categories of theories in different institutions, namely adjunctions, as a means of translating between the different specification spaces that they provide. We show that there is a canonical way in which adjunctions between the categories of signatures can be lifted to the categories of theories. This lifting is associated with a duality between the concepts of institution map and institution morphism. Finally, we make an attempt at generalising these results to institution semi-morphisms that can be presented by an inference system.
This work was partially supported by the Espirit BRA 8035 (MODELAGE), the HCM Scientific Network CHRX-CT92-0054 (MEDICIS), and the contract PRAXIS XXI 2/2.1/MAT/46/94 (ESCOLA).
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
E.Astesiano and M.Cerioli, “Relationships between Logical Frameworks”, in M.Bidoit and C. Choppy (eds) Recent Trends in Data Type Specification, LNCS 655, Springer Verlag 1993, 126–143.
N.Barreiro, J.Fiadeiro and T.Maibaum, “Politeness in Object Societies”, in R.Wieringa and R.Feenstra (eds) Information Systems — Correctness and Reusability, World Scientific Publishing Company 1995, 119–134
R.Burstall and J.Goguen, “Putting Theories together to make Specifications”, in R.Reddy (ed) IJCAI'77, 1977, 1045–1058.
J.Fiadeiro and J.F.Costa, “Institutions for Behaviour Specification”, in E.Astesiano, G.Reggio and A.Tarlecki (eds) Recent Trends in Data Type Specification, LNCS 906, Springer Verlag 1995, 273–289.
J.Fiadeiro and J.F.Costa, “Mirror, Mirror in My Hand: a duality between specifications and models of process behaviour”, Mathematical Structures in Computer Science, in print
J.Fiadeiro and T.Maibaum, “Temporal Reasoning over Deontic Specifications”, in Journal of Logic and Computation 1(3), 1991, 357–395.
J.Fiadeiro and T.Maibaum, “Temporal Theories as Modularisation Units for Concurrent System Specification”, Formal Aspects of Computing 4(3), 1992, 239–272.
J.Fiadeiro and T.Maibaum, “Interconnecting Formalisms: supporting modularity, reuse and incrementality”, in G.E.Kaiser (ed) Proc. 3rd Symposium on Foundations of Software Engineering, ACM Press 1995, 72–80.
J.Goguen and R.Burstall, “Institutions: Abstract Model Theory for Specification and Programming”, Journal of the ACM 39, 1992, 95–146.
R.Goldblatt, Logics of Time and Computation, CSLI, 1987.
S.Khosla and T.Maibaum, “The Prescription and Description of State-Based Systems”, in B.Banieqbal, H.Barringer and A.Pnueli (eds) Temporal Logic in Specification, LNCS 398, Springer-Verlag 1989, 243–294
K.Lano and S.Goldsack, “Refinement, Subtyping and Subclassing in VDM++”, in C.Hankin, I.Makie and R.Nagarajan (eds) Theory and Formal Methods 95, World Scientific Publishing Company 1995
Z.Manna and A.Pnueli, The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag 1991
J.Meseguer, “General Logics”, in H.-D. Ebbinghaus at al (eds) Logic Colloquium 87, North-Holland 1989.
D.Sannella and A.Tarlecki, “Model-theoretic foundations for program development: basic concepts and motivation”, 1995 — extended and expanded version of the paper “Toward formal development of programs from algebraic specifications: modeltheoretic foundations”, in ICALP'92, LNCS 623, 1992, 656–671
V.Sassone, M.Nielsen and G.Winskel, “A Classification of Models for Concurrency”, in E.Best (ed) CONCUR'93, LNCS 715, Springer-Verlag, 82–96.
P.Wolper, “On the Relation of Programs and Computations to Models of Temporal Logic”, in B.Banieqbal, H.Barringer and A.Pnueli (eds) Temporal Logic in Specification, LNCS 398, Springer-Verlag 1989, 75–123.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arrais, M., Fiadeiro, J.L. (1996). Unifying theories in different institutions. In: Haveraaen, M., Owe, O., Dahl, OJ. (eds) Recent Trends in Data Type Specification. ADT COMPASS 1995 1995. Lecture Notes in Computer Science, vol 1130. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61629-2_38
Download citation
DOI: https://doi.org/10.1007/3-540-61629-2_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61629-0
Online ISBN: 978-3-540-70642-7
eBook Packages: Springer Book Archive