Research on "Formal Methods in Computing"

Detecting and Removing Dead-Code using Rank 2 Intersection

ABSTRACT. In this paper we extend, by allowing the use of rank 2 intersection, the "non-standard" type assignment system for the detection and elimination of dead-code in typed functional programs presented by Coppo et al 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. The use of non-standard types (also called "annotated" types) allows 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.

• ps ps.gz ( © Springer-Verlag )

BIBTEX.

@inproceedings{Damiani-Prost:IWT-98,
   author    = {F. Damiani and F. Prost},
   title     = {{Detecting and Removing Dead-Code using Rank 2 Intersection}},
   booktitle = {{International Workshop TYPES'96, Selected Papers}},
   year      = {1998},
   publisher = {Springer},
   pages     = {66-87},
   series    = {LNCS 1512}
}