kirancodes.me
To Proof Maintenance & Beyond!
ASE 2000

Circular Coinductive Rewriting

Joseph A. Goguen, Kai Lin, Grigore Rosu

DOI 10.1109/ase.2000.873657dblp

Abstract

Circular coinductive rewriting is a new method for proving behavioral properties, that combines behavioral rewriting with circular coinduction. This method is implemented in our new BOBJ (Behavioral OBJects) behavioral specification and computation system, which is used in examples throughout this paper. These examples demonstrate the surprising power of circular coinductive rewriting. The paper also sketches the underlying hidden algebraic theory and briefly describes BOBJ and some of its algorithms.

BibTeX
@inproceedings{Goguen-al:ASE00,
  author    = {Joseph A. Goguen and
               Kai Lin and
               Grigore Rosu},
  title     = {Circular Coinductive Rewriting},
  booktitle = {ASE},
  pages     = {123--132},
  publisher = {{IEEE} Computer Society},
  year      = {2000},
}

Related papers