Computability in Europe 2008
Logic and Theory of Algorithms

Print current page  Print this page

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

Edit abstract data

Speaker: Luca Chiarabini
Slot: Tue, 11:20-11:40, Room 22 (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 Valid HTML 4.01! Valid CSS!