Implementing Compositional Analysis Using Intersection Types With Expansion Variables

A program analysis is compositional when the analysis result for a particular program fragment is obtained solely from the results for its immediate subfragments via some composition operator. This means the subfragments can be analyzed independently in any order. Many commonly used program analysis techniques (in ar, most abstract interpretations and most uses of the Hindley/Milner type system) are not compositional and require the entire text of a program for sound and complete analysis. System I is a recent type system for the pure -calculus with intersection types and the new technology of expansion variables. System I supports compositional analysis because it has the principal typings property and an algorithm based on the new technology of -unification has been developed that finds these principal typings. In addition, for each natural number k, typability in the rank-k restriction of System I is decidable, so a complete and terminating analysis algorithm exists for the rank-k ...

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Assaf J. Kfoury, Geoffrey Washburn, Joe Wells
• Keywords: Analysis, ENTCS 2002, Program Analysis, Type System