Skip to main content
SpringerLink
Log in

Comorphism-Based Grothendieck Logics

  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 2002 (MFCS 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2420))

Abstract

In order to obtain a semantic foundation for heterogeneous specification, we extend Diaconescu’s morphism-based Grothendieck institutions to the case of comorphisms. This is not just a dualization, because we obtain more general results, especially concerning amalgamation properties. We also introduce a proof calculus for structured heterogeneous specifications and study its soundness and completeness (where amalgamation properties play a rôle for obtaining the latter).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Arrais and J. L. Fiadeiro. Unifying theories in different institutions. In M. Haveraaen, O. Owe, and O.-J. Dahl (eds.), Proc. 11th WADT, LNCS 1130, p. 81–101. Springer Verlag, 1996.

    Google Scholar 

  2. S. Autexier, D. Hutter, H. Mantel, and A. Schairer. Towards an evolutionary formal software-development using Casl. In C. Choppy and D. Bert (eds.), Proc. 14th WADT, LNCS 1827, p. 73–88. Springer-Verlag, 2000.

    Google Scholar 

  3. S. Autexier and T. Mossakowski. Integrating HOL-Casl into the development graph manager Maya. In FroCoS 2002, LNCS 2309, p. 2–17. Springer, 2002.

    Google Scholar 

  4. H. Baumeister and A. Zamulin. State-based extension of Casl. In Proceedings IFM 2000, LNCS 1945. Springer-Verlag, 2000.

    Google Scholar 

  5. T. Borzyszkowski. Logical systems for structured specifications. Theoretical Computer Science, to appear.

    Google Scholar 

  6. M. Cerioli and J. Meseguer. May I borrow your logic? (transporting logical structures along maps). Theoretical Computer Science, 173:311–347, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  7. S. Coudert, G. Bernot, and P. Le Gall. Hierarchical heterogeneous specifications. In J. L. Fiadeiro (ed.), Proc. 13th WADT, LNCS 1589, p. 106–120. Springer, 1999.

    Google Scholar 

  8. R. Diaconescu. Grothendieck institutions. Applied categorical structures. to appear.

    Google Scholar 

  9. R. Diaconescu and K. Futatsugi. Logical semantics of CafeOBJ. Technical report, JAIST, 1996. IS-RR-96-0024S.

    Google Scholar 

  10. R. Diaconescu, J. Goguen, and P. Stefaneas. Logical support for modularisation. In G. Huet and G. Plotkin (eds.), Proc. of a Workshop on Logical Frameworks, 1991.

    Google Scholar 

  11. F. Durán and J. Meseguer. Structured theories and institutions. In M. Hofmann, G. Rosolini, and D. Pavlovic (eds.), CTCS’ 99, ENTCS 29, 1999.

    Google Scholar 

  12. H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 2 Springer Verlag, Heidelberg, 1990.

    MATH  Google Scholar 

  13. J. Goguen and G. Rosu. Institution morphisms. Formal aspects of computing, to appear, 2001.

    Google Scholar 

  14. J. A. Goguen and R. M. Burstall. Institutions: Abstract model theory for specification and programming. JACM, 39:95–146, 1992.

    Article  MATH  Google Scholar 

  15. J. A. Goguen and W. Tracz. An implementation-oriented semantics for module composition. In G. T. Leavens and M. Sitaraman (eds.), Foundations of Component-Based Systems, p. 231–263. Cambridge University Press, 2000.

    Google Scholar 

  16. J. Meseguer. General logics. In Logic Colloquium 87, p. 275–329. North Holland, 1989.

    Article  MathSciNet  Google Scholar 

  17. T. Mossakowski. Heterogeneous development graphs and heterogeneous borrowing. In M. Nielsen et al. (eds.), Fossacs 2002, LNCS 2303, p. 326–341. Springer, 2002.

    Google Scholar 

  18. T. Mossakowski, S. Autexier, and D. Hutter. Extending development graphs with hiding. In H. Hußmann (ed.), FASE 2001, LNCS 2029, p. 269–283. Springer, 2001.

    Google Scholar 

  19. P. D. Mosses. CoFI: The Common Framework Initiative for Algebraic Specification and Development. In TAPSOFT’ 97, LNCS 1214, p. 115–137. Springer, 1997.

    Google Scholar 

  20. G. Reggio, E. Astesiano, and C. Choppy. Casl-LTL-a Casl extension for dynamic reactive systems-summary. Technical Report of DISI-Università di Genova, DISI-TR-99-34, Italy, 2000.

    Google Scholar 

  21. D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation, 76:165–210, 1988.

    Article  MathSciNet  MATH  Google Scholar 

  22. A. Tarlecki. Moving between logical systems. In M. Haveraaen, O. Owe, and O.-J. Dahl (eds.), Proc. 11th WADT, LNCS 1130, p. 478–502. Springer Verlag, 1996.

    Google Scholar 

  23. A. Tarlecki. Towards heterogeneous specifications. In D. Gabbay and M. d. Rijke (eds.), FroCos 98, Studies in Logic and Computation, p. 337–360. RSP, 2000.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. BISS, Dept. of Computer Science, University of Bremen, Germany

    Till Mossakowski

Authors
  1. Till Mossakowski
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Informatics, Warsaw University, ul. Banacha 2, 02-097, Warszawa, Poland

    Krzysztof Diks  & Wojciech Rytter  & 

  2. Department of Computer Science, Liverpool University, Peach Street, Liverpool, L69 7ZF, UK

    Wojciech Rytter

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mossakowski, T. (2002). Comorphism-Based Grothendieck Logics. In: Diks, K., Rytter, W. (eds) Mathematical Foundations of Computer Science 2002. MFCS 2002. Lecture Notes in Computer Science, vol 2420. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45687-2_49

Download citation

  • DOI: https://doi.org/10.1007/3-540-45687-2_49

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44040-6

  • Online ISBN: 978-3-540-45687-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation