Skip to Main content Skip to Navigation

Réécriture et compilation de confiance

Abstract : Most computer processes involve the notion of transformation, in particular the compilation processes. We interest in this thesis in providing tools and methods, based on rewriting, giving the opportunity to increase the confidence we can place into those processes. We develop first a framework used to validate the compilation of matching constructs, building a formal proof of the validity of the compilation process along with a witness of this proof, for each run of the compiler. Then, in order to allow one to write safely complex transformations, we propose a tool that generates an efficient data structure integrating algebraic invariants, as well as a strategy language that enables to control the application of transformations. Those results can be seen as a first step towards the constitution of generic and safe methods for the development of trustworthy transformations.
Document type :
Complete list of metadata

Cited literature [32 references]  Display  Hide  Download
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 1:57:41 PM
Last modification on : Saturday, October 16, 2021 - 11:26:09 AM


Files produced by the author(s)


  • HAL Id : tel-01752777, version 1



Antoine Reilles. Réécriture et compilation de confiance. Autre [cs.OH]. Institut National Polytechnique de Lorraine, 2006. Français. ⟨NNT : 2006INPL084N⟩. ⟨tel-01752777⟩



Record views


Files downloads