Cyclic Proofs for iGL via Corecursion

Daniyar Shamkanov proved that three distinct systems of sequent calculi for GL are equivalent. These systems consist in one with finite proofs, another with ill-founded proofs and the last one with cyclic proofs. The main tool used for proving the equivalence is corecursion. In this project, we prove the equivalence between a finitary sequent calculus for iGL and a cyclic calculus, using also coinductive methods.