Detecting and Removing Dead Code using Rank 2 Intersection - LARA - Libre accès aux rapports scientifiques et techniques Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1997

Detecting and Removing Dead Code using Rank 2 Intersection

Résumé

In this paper we extend, by allowing rank 2 intersection types, the type assignment system for the detection and elimination of dead code in typed functional programs presented by Coppo et al Giannini and the first author in the Static Analysis Symposium'96.The main application of this method is the optimization of programs extracted from proofs in logical frameworks, but it could be used as well in the elimination of dead code determined by program specialization. This system rely on annotated types which allow to exploit the type structure of the language for the investigation of program properties. The detection of dead code is obtained via annotated type inference, which can be performed in a complete way, by reducing it to the solution of a system of inequalities between annotation variables. Even though the language considered in the paper is the simply typed lambda-calculus with cartesian product, if-then-else, fixpoint, and arithmetic constants we can generalize our approach to polymorphic languages like Miranda, Haskell, and CAML.
Dans ce papier nous étendons, en permettant des types d'intersections de rang 2, un système d'inférence de types pour la détection et l'élimination du code mort dans les programmes fonctionnels typés présenté par Coppo et al Giannini dans le Static Analysis Symposium'96. La principale application de cette méthode est l'optimisation de programmes extraits de preuves, mais il peut aussi bien être utilisé pour l'élimination du code mort produit par la spécialisation de programmes. Ce système repose sur des types annotés qui permettent d'exploiter la structure des types du langage pour trouver des propriétés sur un programme. La détection du code mort est obtenue via un système d'inférence de types. L'inférence peut être réalisée en réduisant le problème à la solution d'un système d'inégalités entre les variables d'annotations. Bien que le langage considéré soit le lambda-calcul simplement typé étendu par le produit cartésien, le if-then-else, le point fixe et des constantes arithmétiques, nous pouvons généraliser notre approche aux langages polymorphes tels que Miranda, Haskell et CAML.
Fichier principal
Vignette du fichier
RR1997-10.pdf (374.08 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02101840 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02101840 , version 1

Citer

Frederic Prost. Detecting and Removing Dead Code using Rank 2 Intersection. [Research Report] LIP RR-1997-10, Laboratoire de l'informatique du parallélisme. 1997, 2+23p. ⟨hal-02101840⟩
11 Consultations
158 Téléchargements

Partager

Gmail Facebook X LinkedIn More