A Modular, Polyvariant, and Type-Based Closure Analysis

We observe that the principal typing property of a type system is the enabling technology for modularity and separate compilation [10]. We use this technology to formulate a modular and polyvariant closure analysis, based on the rank 2 intersection types annotated with control-flow information. Modularity manifests itself in a syntax-directed, annotated-type inference algorithm that can analyse program fragments containing free variables: a principal typing property is used to formalise it. Polyvariance manifests itself in the separation of different behaviours of the same function at its different uses: this is formalised via the rank 2 intersection types. As the rank 2 intersection type discipline types at least all (core) ML programs, our analysis can be used in the separate compilation of such programs.

• Type: Conference
• Year: 1997
• Where: ICFP
• Authors: Anindya Banerjee
• Keywords: ICFP 1997, Intersection Type, Principal Typing Property, Programming Languages, Separate Compilation