Computability in Europe 2006
Logical Approaches to Computational Barriers

Regular Talk:
Extraction of Efficient Programs from Correct Proofs: The Case of Structural Induction over Natural Numbers

Speaker: Luca Chiarabini
Slot: Array, 11:20-11:40, col. 4


Transforming a  recursive program into a tail recursive one brings many
computationally benefits; in particular in each recursive step there is no
context information to store. In this paper we consider the particularly simple
induction schema over natural numbers, and we propose
two methods to automatically turn it into another proof with tail recursive
content: one ``continuation'' and one ``accumulator'' based.

websites: Arnold Beckmann 2008-05-19