Advertisement

Unifying theories in different institutions

  • M. Arrais
  • J. L. Fiadeiro
Contributions
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1130)

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.

Keywords

Inference System Temporal Logic Natural Transformation Linear Temporal Logic Left Adjoint 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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.Google Scholar
  2. 2.
    N.Barreiro, J.Fiadeiro and T.Maibaum, “Politeness in Object Societies”, in R.Wieringa and R.Feenstra (eds) Information SystemsCorrectness and Reusability, World Scientific Publishing Company 1995, 119–134Google Scholar
  3. 3.
    R.Burstall and J.Goguen, “Putting Theories together to make Specifications”, in R.Reddy (ed) IJCAI'77, 1977, 1045–1058.Google Scholar
  4. 4.
    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.Google Scholar
  5. 5.
    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 printGoogle Scholar
  6. 6.
    J.Fiadeiro and T.Maibaum, “Temporal Reasoning over Deontic Specifications”, in Journal of Logic and Computation 1(3), 1991, 357–395.Google Scholar
  7. 7.
    J.Fiadeiro and T.Maibaum, “Temporal Theories as Modularisation Units for Concurrent System Specification”, Formal Aspects of Computing 4(3), 1992, 239–272.Google Scholar
  8. 8.
    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.Google Scholar
  9. 9.
    J.Goguen and R.Burstall, “Institutions: Abstract Model Theory for Specification and Programming”, Journal of the ACM 39, 1992, 95–146.Google Scholar
  10. 10.
    R.Goldblatt, Logics of Time and Computation, CSLI, 1987.Google Scholar
  11. 11.
    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–294Google Scholar
  12. 12.
    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 1995Google Scholar
  13. 13.
    Z.Manna and A.Pnueli, The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag 1991Google Scholar
  14. 14.
    J.Meseguer, “General Logics”, in H.-D. Ebbinghaus at al (eds) Logic Colloquium 87, North-Holland 1989.Google Scholar
  15. 15.
    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–671Google Scholar
  16. 16.
    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.Google Scholar
  17. 17.
    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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • M. Arrais
    • 1
  • J. L. Fiadeiro
    • 2
  1. 1.Sistemas Informáticos S.A.EDINFORSacavém CodexPortugal
  2. 2.Department of Informatics, Faculty of SciencesUniversity of LisbonLisboaPortugal

Personalised recommendations