Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Pattern eliminating transformations

Horatiu Cirstea 1 Pierre Lermusiaux 2 Pierre-Etienne Moreau 1
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
Abstract : Program transformation is a common practice in computer science, and its many applications can have a range of different objectives. For example, a program written in an original high level language could be either translated into machine code for execution purposes, or towards a language suitable for formal verification. Such compilations are split into several so-called passes which generally aim at eliminating certain constructions of the original language to get some intermediate languages and finally generate the target code. Rewriting is a widely established formalism to describe the mechanism and the logic behind such transformations. In a typed context featuring type-preserving rewrite rules, the underlying type system can be used to give syntactic guarantees on the shape of the results obtained after each pass, but this approach could lead to an accumulation of (auxiliary) types that should be considered. We propose in this paper an approach where the function symbols corresponding to the transformations performed in a pass are annotated with the (anti-)patterns they are supposed to eliminate and show how we can check that the transformation is consistent with the annotations and thus, that it eliminates the respective patterns. With the generic principles governing term algebra and rewriting, we believe this approach to be an accurate formalism to any language providing pattern-matching primitives.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download
Contributor : Pierre Lermusiaux <>
Submitted on : Thursday, February 13, 2020 - 7:20:40 PM
Last modification on : Saturday, February 15, 2020 - 1:36:36 AM
Document(s) archivé(s) le : Thursday, May 14, 2020 - 6:18:40 PM


Files produced by the author(s)


  • HAL Id : hal-02476012, version 2



Horatiu Cirstea, Pierre Lermusiaux, Pierre-Etienne Moreau. Pattern eliminating transformations. 2020. ⟨hal-02476012v2⟩



Record views


Files downloads