Inductive Fixpoints in Higher Order Logic

2004.

Cited by: 2|Bibtex|Views0|
Keywords:
higher order logic

Abstract:

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.

Code:

Data:

Your rating :
0

 

Tags
Comments