A complete coinductive logical system for bisimulation equivalence on circular objects

We introduce a coinductive logical system a la Gentzen for establishing bisimulation equivalences on circular non-wellfounded regular objects, inspired by work of Coquand, and of Brandt and Henglein. In order to describe circular objects, we utilize a typed language, whose coinductive types involve disjoint sum, cartesian product, and finite powerset constructors. Our system is shown to be complete with respect to a maximal fixed point semantics. It is shown to be complete also with respect to an equivalent final semantics. In this latter semantics, terms are viewed as points of a coalgebra for a suitable endofunctor on the category Set* of non-wellfounded sets. Our system subsumes an axiomatization of regular processes, alternative to the classical one given by Milner.