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

Abstract

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