Refinement types for program analysis

  • Mario Coppo
  • Ferruccio Damiani
  • Paola Giannini
Contributed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1145)


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.


Type Inference Type Assignment Faithful Refinement Faithful Typing Binding Time 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    H. P. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48:931–940, 1983.Google Scholar
  2. 2.
    S. Berardi. Pruning Simply Typed Lambda Terms. Journal of Symbolic Computation, to appear.Google Scholar
  3. 3.
    S. Berardi and L. Boerio. Using Subtyping in Program Optimization. In Typed Lambda Calculus and Applications, 1995.Google Scholar
  4. 4.
    M. Coppo and M. Dezani-Ciancaglini. An extension of basic functional theory for lambda-calculus. Notre Dame Journal of Formal Logic, 21(4):685–693, 1980.Google Scholar
  5. 5.
    M. Coppo and A. Ferrari. Type inference, abstract interpretation and strictness analysis. In M. Dezani-Ciancaglini et al., editors, A collection of contributions in honour of Corrado Böhm, pages 113–145. Elsevier, 1993.Google Scholar
  6. 6.
    M. Coppo and P. Giannini. Pricipal Types and Unification for Simple Intersection Types Systems. Information and Computation, 122(1):70–96, 1995.Google Scholar
  7. 7.
    F. Damiani and P. Giannini. A Decidable Intersection Type System based on Relevance. In Theoretical Aspects of Computer Software, LNCS 789. Springer, 1994.Google Scholar
  8. 8.
    C. Hankin and D. Le Metayer. A Type-Based Framework for Program Analysis. In Static Analisys, LNCS 864, pages 380–394. Springer, 1994.Google Scholar
  9. 9.
    R. Hindley. The principal types schemes for an object in combinatory logic. Transactions of American Mathematical Society, 146:29–60, 1969.Google Scholar
  10. 10.
    L.S. Hunt and D. Sands. Binding Time Analysis: A New PERspective. In Proceedings of the ACM Symposium on Partial Evaluation and Semantics-based Program Manipulation, 1991.Google Scholar
  11. 11.
    P. O'Keefe J. Palsberg. A Type System Equivalent to Flow Analysis. In Principles of Programming Languages, 1995.Google Scholar
  12. 12.
    T. P. Jensen. Strictness Analysis in Logical Form. In J. Hughes, editor, Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture, pages 98–105, 1991.Google Scholar
  13. 13.
    H. R. Nielson K. L. Solberg and F. Nielson. Strictness and Totality Analysis. In Static Analisys, LNCS 864, pages 408–422. Springer, 1994.Google Scholar
  14. 14.
    D. Leivant. Polymorphic Type Inference. In Principles of Programming Languages, ACM, 1983.Google Scholar
  15. 15.
    R. Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and System Science, 17:348–375, 1978.CrossRefGoogle Scholar
  16. 16.
    F. Prost. Marking techniques for extraction. Technical report, Ecole Normale Supérieure de Lyon, Lyon, December 1995.Google Scholar
  17. 17.
    T.M.Kuo and P.Mishra. Strictness analysis: a new perspective based on type inference. In Functional Programming Languages and Computer Architecture. ACM, 1989.Google Scholar
  18. 18.
    D. A. Wright. A New Technique for Strictness Analysis. In Proceedings of TAP-SOFT'91, LNCS 494, pages 260–272. Springer, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Mario Coppo
    • 1
  • Ferruccio Damiani
    • 1
  • Paola Giannini
    • 1
  1. 1.Dipartimento di InformaticaUniversità di TorinoTorinoItaly

Personalised recommendations