Exercises in coinduction and coalgebraic specification

Bart Jacobs and Jan Rutten

www.cs.kun.nl/~bart and www.cwi.nl/~janr).

On coagebra in general
J.J.M.M. Rutten Universal coalgebra: a theory of systems. Technical Report CS-R9652, CWI, Amsterdam, 1996. To appear in Theoretical Computer Science.

B. Jacobs and J.J.M.M. Rutten A Tutorial on (Co)Algebras and (Co)Induction. Bulletin of EATCS Vol. 62, 1997, pp. 222--259.

B. Jacobs, L. Moss, H. Reichel and J.J.M.M. Rutten (editors) Proceedings of First Workshop on Coalgebraic Methods in Computer Science (CMCS '98). ENTCS Volume 11 , Elsevier Science B.V., 1998.

B. Jacobs and J.J.M.M. Rutten (editors) Proceedings of Second Workshop on Coalgebraic Methods in Computer Science (CMCS '99). ENTCS Volume 19 , Elsevier Science B.V., 1999.

On coalgebraic specification
B. Jacobs Objects and Classes, Co-algebraically. In: B. Freitag and C.B. Jones and C. Lengauer and H.-J. Schek (eds) Object-Orientation with Parallelism and Persistence, Kluwer Acad. Publ. 1996, 83--103

B. Jacobs Invariants, Bisimulations and the Correctness of Coalgebraic Refinements In: M. Johnson (ed), Algebraic Methodology and Software Technology, Springer LNCS 1349, 1997, 276--291.

B. Jacobs, Coalgebras in Specification and Verification for Object-Oriented Languages. In: Newsletter 3 of the Dutch Association for Theoretical Computer Science (NVTI), see http://www.cs.kun.nl/~bart/PAPERS/nvti99.ps.Z.

On definitions and proofs by coinduction
J.J.M.M. Rutten Automata and coinduction (an exercise in coalgebra). Technical Report SEN-R9803, CWI, Amsterdam, 1998. Also in: Proceedings of CONCUR '98, D. Sangiorigi and R. de Simone (eds.), LNCS 1466, Springer, 1998, pp. 194-218.

J.J.M.M. Rutten Automata, power series, and coinduction: taking input derivatives seriously (extended abstract). Technical Report SEN-R9901, CWI, Amsterdam, 1999. Also in: proceedings of ICALP '99 (J. Wiedermann, P. van Emde Boas and M. Nielsen, eds.), LNCS 1644, Springer, 1999, pp. 645-654.

J.J.M.M. Rutten A note on coinduction and weak bisimilarity for while programs. Technical Report SEN-R9826, CWI, Amsterdam, 1998. To appear in RAIRO - Theoretical Informatics and Applications.