Sciweavers

SOFSEM
2009
Springer

From Outermost Termination to Innermost Termination

14 years 15 days ago
From Outermost Termination to Innermost Termination
Abstract. Rewriting is the underlying evaluation mechanism of functional programming languages. Therefore, termination analysis of term rewrite systems (TRSs) is an important technique for program verification. To capture the evaluation mechanism of a programming language one has to take care of the evaluation strategy, where we focus on the outermost strategy. As there are only few techniques available to analyze outermost termination of TRSs directly, we introduce a new transformation such that a TRS is outermost terminating iff the transformed TRS is innermost terminating. In this way all of the several techniques that have been developed to investigate innermost termination become applicable to analyze outermost termination, too. We have implemented the transformation and successfully evaluated it on a large collection of TRSs.
René Thiemann
Added 17 Mar 2010
Updated 17 Mar 2010
Type Conference
Year 2009
Where SOFSEM
Authors René Thiemann
Comments (0)