Circular Coinductive Rewriting

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 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.

• Type: Conference
• Year: 2000
• Where: KBSE
• Authors: Joseph A. Goguen, Kai Lin, Grigore Rosu
• Keywords: BOBJ Behavioral Specification, Circular Coinduction, Circular Coinductive Rewriting, KBSE 2000, Software Engineering