Making progress: Reducibility Candidates and Cut Elimination in the Ill-founded Realm

Gianluca Curzi, Graham E. Leigh

Ill-founded (or non-wellfounded) proof systems have emerged as a natural framework for inductive and coinductive reasoning. In such systems, soundness relies on global correctness…