Detecting and Removing Dead Code using Rank 2 Intersection

Abstract : 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.
Document type :
Reports
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101840
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:07:50 AM
Last modification on : Wednesday, November 20, 2019 - 2:54:30 AM

File

RR1997-10.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101840, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

11

Files downloads

36