Behavioral and coinductive rewriting

Joseph Goguen, Kai Lin, Grigore Roşu

Research output: Contribution to journalConference articlepeer-review


Behavioral rewriting differs from standard rewriting in taking account of the weaker inference rules of behavioral logic, but it shares much with standard rewriting, including notions like termination and confluence. We describe an efficient implementation of behavioral rewriting that uses standard rewriting. Circular coinductive rewriting combines behavioral rewriting with circular coinduction, giving a surprisingly powerful proof method for behavioral properties; it is implemented in the BOBJ system, which is used in our examples. These include several lazy functional stream program equivalences and a behavioral refinement.

Original languageEnglish (US)
Pages (from-to)2-23
Number of pages22
JournalElectronic Notes in Theoretical Computer Science
StatePublished - 2000
Externally publishedYes
EventThe 3rd International Workshop on Rewriting Logic and its Applications - Kanzawa, Japan
Duration: Sep 18 2000Sep 20 2000

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Behavioral and coinductive rewriting'. Together they form a unique fingerprint.

Cite this