Inductive Fixpoints in Higher Order Logic
Sava Krstić · 2004
We show that an analogue of the domain-theoretic least fixpoint operator can be defined in a purely set-theoretic framework. It can be formalized in classical higher order logic, serving as a solid foundation for proving termination of (possibly nested) recursive programs in a variety of mechanized proof systems.