  The aim of the paper is to provide solid foundations for a programming
paradigm natively supporting the creation and manipulation of cyclic data
structures. To this end, we describe coFJ, a Java-like calculus where objects
can be infinite and methods are equipped with a codefinition (an alternative
body). We provide an abstract semantics of the calculus based on the framework
of inference systems with corules. In coFJ with this semantics, FJ recursive
methods on finite objects can be extended to infinite objects as well, and
behave as desired by the programmer, by specifying a codefinition. We also
describe an operational semantics which can be directly implemented in a
programming language, and prove the soundness of such semantics with respect to
the abstract one.
