@inproceedings{64fb0039be6d4e2cb4fe18db0ba3b1e5,
title = "Refinement types for program analysis",
abstract = "In this paper we introduce a system for the detection and elimination of dead code in typed functional programs. 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. Our algorithm is based on a type inference system suitable for reasoning about dead code information. This system relays on refinement 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 type inference, which can be performed in an efficient and complete way, by reducing it to the solution of a system of inequalities between type variables. A key feature of our method is that program analysis can be performed in a strictly incremental way. Even though the language considered in the paper is a simply typed λ-calculus we can generalize our approach to polymorphic languages like ML. Although focused on dead code elimination our type inference method can also be applied to the investigation of other program properties like binding time and strictness. Some hints on these applications are given.",
author = "Mario Coppo and Ferruccio Damiani and Paola Giannini",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1996.; 3rd International Static Analysis Symposium, SAS 1996 ; Conference date: 24-09-1996 Through 26-09-1996",
year = "1996",
doi = "10.1007/3-540-61739-6\_39",
language = "English",
isbn = "3540617396",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "143--158",
editor = "Radhia Cousot and Schmidt, \{David A.\}",
booktitle = "Static Analysis - 3rd International Symposium, SAS 1996, Proceedings",
address = "Germany",
}