Algebraic-co-algebraic specification in CoCASL (bibtex)

by Till Mossakowski, Horst Reichel, Markus Roggenbach and Lutz Schröder

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.

View PDF

Reference:

Till Mossakowski, Horst Reichel, Markus Roggenbach and Lutz Schröder: Algebraic-co-algebraic specification in CoCASL, In Martin Wirsing, Dirk Pattinson, Rolf Hennicker, eds.: Recent Developments in Algebraic Development Techniques, 16th International Workshop, WADT'02, Lecture Notes in Computer Science, vol. 2755, pp. 376–392, Springer; Berlin; http://www.springer.de, 2003. [preprint]

Bibtex Entry:

@InProceedings{MossakowskiEA03,
  author = {Till Mossakowski and Horst Reichel and Markus Roggenbach and Lutz Schr{\"o}der},
  title = {Algebraic-co-algebraic specification in {CoCASL}},
  year = {2003},
  editor = {Martin Wirsing and Dirk Pattinson and Rolf Hennicker},
  booktitle = {Recent Developments in Algebraic Development Techniques, 16th International Workshop, WADT'02},
  publisher = {Springer; Berlin; http://www.springer.de},
  series = {Lecture Notes in Computer Science},
  volume = {2755},
  pages = {376--392},
  keywords = {CASL coalgebra modal logic CoCASL},
  url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2755&spage=376},
  comment = { <a href = "http://www.informatik.uni-bremen.de/~till/papers/cocasl.pdf"> [preprint] </a>},
  psurl = {http://www8.informatik.uni-erlangen.de/~schroeder/papers/cocasl.ps},
  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.
},
}