Abstract: 
Tailrecursive function definitions are sometimes more straightforward than
alternatives, but proving theorems on them may be roundabout because of the
peculiar form of the resulting recursion induction rules.
This paper describes a proof method that provides a general solution to
this problem by means of suitable invariants over inductive sets, and
illustrates the application of such method by examining two case studies.

BibTeX: 
@article{Tail_Recursive_FunctionsAFP,
author = {Pasquale Noce},
title = {A General Method for the Proof of Theorems on Tailrecursive Functions},
journal = {Archive of Formal Proofs},
month = dec,
year = 2013,
note = {\url{http://isaafp.org/entries/Tail_Recursive_Functions.html},
Formal proof development},
ISSN = {2150914x},
}
