  In this paper we introduce a cut-free sequent calculus for the
alternation-free fragment of the modal $\mu$-calculus. This system allows for
cyclic proofs and uses a simple focus mechanism to control the unravelling of
fixpoints along infinite branches. We show that the proof system is sound and
complete and apply it to prove that the alternation-free fragment has the Craig
interpolation property.
