Skip to Main content Skip to Navigation
Theses

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 :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/SCD_T_2003_0176_FISSORE.pdf
Complete list of metadata

https://hal.univ-lorraine.fr/tel-01746842
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 10:45:55 AM
Last modification on : Tuesday, September 29, 2020 - 11:49:13 AM

Identifiers

  • HAL Id : tel-01746842, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

53