We introduce a generalized notion of inference system to support structural recursion on non
well-founded datatypes. Besides axioms and inference rules with the usual meaning, a
generalized inference system allows coaxioms, which are, intuitively, axioms which can only
be applied “at infinite depth” in a proof tree. This notion nicely subsumes standard inference
systems and their inductive and coinductive interpretation, while providing more flexibility.
Indeed, the classical results on the existence and constructive characterization of least and …

After surveying classical results, we introduce a generalized notion of inference system to
support structural recursion on non-well-founded data types. Besides axioms and inference
rules with the usual meaning, a generalized inference system allows coaxioms, which are,
intuitively, axioms which can only be applied" at infinite depth" in a proof tree. This notion
nicely subsumes standard inference systems and their inductive and coinductive
interpretation, while providing more flexibility. Indeed, the classical results can be extended …