Course-of-values recursion in Martin-Löf's type theory

Abstract

To facilitate reasoning about programs in Martin Löf’s Type Theory, the introduction general recursion operators has been studied. This allow a more conventional programming style, being possible to separte the termination proof of the program from the proof of other properties. This work experiments with this idea studying Course-of-Values induction for Natural Numbers. An introduction rule is derived from natural induction, obtaining an expression for a recursion operator. A propositional equality that expresses the behavior of the obtained operator is proved. This equality will be usefull when proving properties of programs. ALF is used as editor of Martin Löf’s monomorphic Set Theory and checker of all the proofs.