×

Generalized theoroidal institution comorphisms. (English) Zbl 1253.68226

Corradini, Andrea (ed.) et al., Recent trends in algebraic development techniques. 19th international workshop, WADT 2008, Pisa, Italy, June 13–16, 2008. Revised selected papers. Berlin: Springer (ISBN 978-3-642-03428-2/pbk). Lecture Notes in Computer Science 5486, 88-101 (2009).
Summary: We propose a generalization of the notion of theoroidal comorphism, motivated by several logic translations of practical importance, encountered in the implementation of the heterogeneous tool set Hets. We discuss the impact of this generalization on the level of heterogeneous specifications, by presenting the Grothendieck construction over a diagram of institutions and translations modelled as generalized comorphisms. Conditions for heterogeneous proofs are also evaluated.
For the entire collection see [Zbl 1173.68005].

MSC:

68Q65 Abstract data types; algebraic specification
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Cerioli, M., Haxthausen, A., Krieg-Brückner, B., Mossakowski, T.: Permissive subsorted partial logic in CASL. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 91–107. Springer, Heidelberg (1997) · Zbl 0886.03022
[2] Cornelius, F., Baldamus, M., Ehrig, H., Orejas, F.: Abstract and behaviour module specifications. Mathematical Structures in Computer Science 9(1), 21–62 (1999) · Zbl 0923.68089
[3] Diaconescu, R.: Grothendieck institutions. Applied categorical structures 10, 383–402 (2002) · Zbl 1008.68078
[4] Ehrig, H., Pepper, P., Orejas, F.: On recent trends in algebraic specification. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989, vol. 372, pp. 263–288. Springer, Heidelberg (1989) · Zbl 0689.68013
[5] Goguen, J., Roşu, G.: Institution morphisms. Formal aspects of computing 13, 274–307 (2002) · Zbl 1001.68019
[6] Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39, 95–146 (1992) · Zbl 0799.68134
[7] Jones, S.P.: Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge (2003) · Zbl 1067.68041
[8] Lüth, C., Roggenbach, M., Schröder, L.: CCC - the CASL consistency checker. In: Fiadeiro, J.L., Mosses, P.D., Orejas, F. (eds.) WADT 2004. LNCS, vol. 3423, pp. 94–105. Springer, Heidelberg (2005) · Zbl 1118.68558
[9] Lüttich, K., Mossakowski, T.: Reasoning Support for CASL with Automated Theorem Proving Systems. In: Fiadeiro, J.L., Schobbens, P.-Y. (eds.) WADT 2006. LNCS, vol. 4409, pp. 74–91. Springer, Heidelberg (2007) · Zbl 1196.68147
[10] Lutz, C., Walther, D., Wolter, F.: Conservative extensions in expressive description logics. In: Proc. of IJCAI 2007, pp. 453–459. AAAI Press, Menlo Park (2007)
[11] Meseguer, J.: General logics. In: Logic Colloquium 1987, pp. 275–329. North Holland, Amsterdam (1989)
[12] Mossakowski, T.: Representations, hierarchies and graphs of institutions. PhD thesis, Universität Bremen, Also appeared as book in Logos Verlag (1996)
[13] Mossakowski, T.: Comorphism-based Grothendieck logics. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 593–604. Springer, Heidelberg (2002) · Zbl 1014.68098
[14] Mossakowski, T.: Relating CASL with other specification languages: the institution level. Theoretical Computer Science 286, 367–475 (2002) · Zbl 1061.68106
[15] Mossakowski, T.: Foundations of heterogeneous specification. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 359–375. Springer, Heidelberg (2003) · Zbl 1278.68208
[16] Mossakowski, T.: Heterogeneous specification and the heterogeneous tool set. Technical report, Universitaet Bremen, Habilitation thesis (2005)
[17] Mossakowski, T., Maeder, C., Lüttich, K.: The Heterogeneous Tool Set. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007) · Zbl 05185799
[18] Mosses, P.D. (ed.): Casl Reference Manual: The Complete Documentation of The Common Algebraic Specification Language. LNCS, vol. 2960. Springer, Heidelberg (2004) · Zbl 1046.68001
[19] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131
[20] Schröder, L., Mossakowski, T.: HasCASL: towards integrated specification and development of functional programs. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 99–116. Springer, Heidelberg (2002) · Zbl 1275.68054
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.