A General Method for the Proof of Theorems on Tail-recursive Functions

Title:	A General Method for the Proof of Theorems on Tail-recursive Functions
Author:	Pasquale Noce (pasquale /dot/ noce /dot/ lavoro /at/ gmail /dot/ com)
Submission date:	2013-12-01
Abstract:	Tail-recursive 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_Functions-AFP, author = {Pasquale Noce}, title = {A General Method for the Proof of Theorems on Tail-recursive Functions}, journal = {Archive of Formal Proofs}, month = dec, year = 2013, note = {\url{http://isa-afp.org/entries/Tail_Recursive_Functions.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.