Detecting and Removing Dead Code using Rank 2 Intersection

Frederic Prost (1)

1 LIP - Laboratoire de l'Informatique du Parallélisme

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.

Mots clés: Intersection Types; Annotated Types; Dead-Code Analysis

Mots clés: Analyse de code mort; Types annotés; Types intersection

Domaines: Informatique [cs]

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⟩