We introduce a {\em coinductive} logical system {\em \`a la } Gentzen for 
establishing {\em bisimulation} equivalences on {\em 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
{\em non-wellfounded} sets. 
Our system subsumes an  axiomatization of regular processes, alternative to 
the classical one given by Milner.