Skip to Main content Skip to Navigation

Terminaison de la réécriture sous stratégies

Abstract : The aim of this thesis is to study and develop tools for proving termination of rule-based languages using strategies. Starting from an original method for proving, by induction, the termination of innermost rewriting, we enhanced and extended this method to the outermost and local strategies. These proof processes have then been implemented in a tool, named CARIBOO. Such languages as ELAN make it possible for the programmer to define his own strategies, by combining rules of the program with appropriate strategy operators. We came up with a method allowing to prove termination of such strategies, based on an automatic simplification process. Finally, our original inductive proof process has been adapted to show weak termination of programs. This new process provides both the proof of termination of at least one evaluation of any data and an evaluation algorithm for this data.
Document type :
Complete list of metadata
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 10:45:55 AM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM

Links full text


  • HAL Id : tel-01746842, version 1



Olivier Fissore. Terminaison de la réécriture sous stratégies. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2003. Français. ⟨NNT : 2003NAN10176⟩. ⟨tel-01746842⟩



Record views