Computation by infinite descent made explicit

Sebastian Enqvist

We introduce a non-wellfounded proof system for intuitionistic logic extended with inductive and co-inductive definitions, based on a syntax in which fixpoint formulas are annotate…