Inductive Fixpoints in Higher Order Logic
higher order logic
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 termina- tion of (possibly nested) recursive programs in a variety of mechanized proof systems.
Full Text (Upload PDF)
PPT (Upload PPT)