We present a calculus of ``circular proofs'': the graph underlying a
proof is not a finite tree but instead it is allowed to contain a
certain amount of cycles. The main challenge in developing a theory
for the calculus is to define the semantics of proofs, since the
usual method by induction on the structure is not available. We
solve this problem by associating to each proof a system of
equations -- defining relations among undetermined arrows of an
arbitrary category with finite products and coproducts as well as
constructible initial algebras and final coalgebras -- and by
proving that this system admits always a unique solution. We prove a
cut-elimination theorem which is shown to be compatible with the
semantics.
