Circular Coinductive Rewriting








Circular coinduction is a new technique 
for behavioral reasoning that significantly generalizes coinduction, 
to look even more like the dual 
of induction. We present a new method 
for proving behavioral equivalences which integrates circular 
coinduction with behavioral rewriting. This method has 
been implemented in the behavioral specification language 
BOBJ, the notation of which is used 
throughout the paper, in examples which illustrate 
the power of the method.