Cut Elimination for a Logic with Induction and Co-induction

Alwen Tiu, Alberto Momigliano

Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus…