Inductive Fixpoints in Higher Order Logic
msra(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 termina- tion of (possibly nested) recursive programs in a variety of mechanized proof systems.
更多查看译文
关键词
higher order logic
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络