  We present a sequent-style proof system for provability logic GL that admits
so-called circular proofs. For these proofs, the graph underlying a proof is
not a finite tree but is allowed to contain cycles. As an application, we
establish Lindon interpolation for GL syntactically.
