Abstract
We introduce CoCasl as a simple coalgebraic extension of the algebraic specification language Casl. CoCasl allows the nested combination of algebraic datatypes and coalgebraic process types. We show that the well-known coalgebraic modal logic can be expressed in CoCasl. We present sufficient criteria for the existence of cofree models, also for several variants of nested cofree and free specifications. Moreover, we describe an extension of the existing proof support for Casl (in the shape of an encoding into higher-order logic) to CoCasl.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Adámek, J., Herrlich, H., Strecker, G.E.: Abstract and concrete categories. Wiley Interscience, Hoboken (1990)
Arbib, M., Manes, E.: Parametrized data types do not need highly constrained parameters. Inform. Control 52, 139–158 (1982)
Barr, M.: Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci. 114, 299–315 (1993)
Bidoit, M., Hennicker, R.: On the integration of observability and reachability concepts. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 21–36. Springer, Heidelberg (2002)
Bidoit, M., Hennicker, R., Kurz, A.: Observational logic, constructor-based logic, and their duality. Theoret. Comput. Sci. 298, 471–510 (2003)
Burmeister, P.: Partial algebras – survey of a unifying approach towards a twovalued model theory for partial algebras. Algebra Universalis 15, 306–358 (1982)
Cîrstea, C.: On specification logics for algebra-coalgebra structures: Reconciling reachability and observability. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 82–97. Springer, Heidelberg (2002)
Cockett, R., Fukushima, T.: About Charity, Yellow Series Report 92/480/18, Univ. of Calgary, Dept. of Comp. Sci. (1992)
Jones, S.P., et al.: Haskell 98: A non-strict, purely functional language (1999), http://www.haskell.org/onlinereport
Goguen, J., Lin, K., Rosu, G.: Conditional circular coinductive rewriting. In: Automated Software Engineering, pp. 123–131. IEEE Press, Los Alamitos (2000)
Goguen, J.A.: Hidden algebraic engineering. In: Nehaniv, C., Ito, M. (eds.) Algebraic Engineering, pp. 17–36. World Scientific, Singapore (1999)
Gumm, H.P., Schröder, T.: Coalgebras of bounded type. Math. Struct. Comput. Sci. 12, 565–578 (2002)
Kozen, D.: Results on the propositional mu -calculus. Theoret. Comput. Sci. 27, 333–354 (1983)
Kurz, A.: Specifying coalgebras with modal logic. Theoret. Comput. Sci. 260, 119–138 (2001)
Kurz, A.: Logics admitting final semantics. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 238–249. Springer, Heidelberg (2002)
Mossakowski, T.: Casl: From semantics to tools. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 93–108. Springer, Heidelberg (2000)
Mossakowski, T.: Relating Casl with other specification languages: the institution level. Theoret. Comput. Sci. 286, 367–475 (2002)
Mossakowski, T., Roggenbach, M., Schröder, L.: CoCasl at work – modelling process algebra. In: CMCS 2003. ENTCS, vol. 82(1) (2003)
Mossakowski, T., Schröder, L., Roggenbach, M., Reichel, H.: Algebraic-coalgebraic specification in CoCasl, Tech. report, University of Bremen, available at http://www.informatik.uni-bremen.de/~lschrode/papers/cocasl.ev.ps
Mosses, P.D. (ed.): Casl – the common algebraic specification language. Reference manual. Springer, Heidelberg (to appear)
Pattinson, D.: Expressive logics for coalgebras via terminal sequence induction, Tech. report, LMU München (2002)
Reichel, H.: An approach to object semantics based on terminal co-algebras. Math. Struct. Comput. Sci. 5, 129–152 (1995)
Reichel, H.: A uniform model theory for the specification of data and process types. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 348–365. Springer, Heidelberg (2000)
Roşu, G.: Hidden logic, Ph.D. thesis, Univ. of California at San Diego (2000)
Rothe, J., Tews, H., Jacobs, B.: The Coalgebraic Class Specification Language CCSL. J. Universal Comput. Sci. 7, 175–193 (2001)
Rutten, J.: Universal coalgebra: A theory of systems. Theoret. Comput. Sci. 249, 3–80 (2000)
Tarlecki, A.: On the existence of free models in abstract algebraic institutions. Theoret. Comput. Sci. 37, 269–304 (1985)
Tews, H.: Coalgebraic methods for object–oriented languages, Ph.D. thesis, Dresden Univ. of Technology (2002)
van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mossakowski, T., Reichel, H., Roggenbach, M., Schröder, L. (2003). Algebraic-Coalgebraic Specification in CoCasl . In: Wirsing, M., Pattinson, D., Hennicker, R. (eds) Recent Trends in Algebraic Development Techniques. WADT 2002. Lecture Notes in Computer Science, vol 2755. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40020-2_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-40020-2_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20537-1
Online ISBN: 978-3-540-40020-2
eBook Packages: Springer Book Archive