Detecting and removing dead-code using rank 2 intersection

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 nonstandard types (also called annotated types) allows to exploit the type structure of the language for investigating program properties. Dead-code is detected 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 λ-calculus with cartesian product, if-then-else, fixpoint, and arithmetic constants we can generalize our approach to polymorphic languages like Miranda, Haskell, and CAML.