Compositional Analysis

The efforts of the Church Project in Compositional Analysis are currently a collaboration between Church Project members at Heriot-Watt University and Boston University. All of the collaborators at Heriot-Watt belong to the ULTRA group (Useful Logics, Type theories, Rewriting systems and Applications) and some of them also work on the EC-funded DART project (Dynamic Assembly, Reconfiguration, and Type-checking).

Overview

Many of the current forms of program analysis work best when given as input the entire program or system to be analyzed. This includes many forms of type-based analysis. However, by their very nature, large software systems are assembled from components that are designed separately and updated at different times. Hence, in order to do the best possible job of handling large software systems, a methodology for program analysis needs to become compositional, and thereby usable in a modular and incremental fashion.

Type systems for programming languages which are flexible enough to allow safe code-reuse and abstract datatypes must support polymorphic types of one kind or another. Programming languages with polymorphic type systems have generally (starting in the 1980's through now) used types with ∀ ("for all") and ∃ ("there exists") quantifiers or closely related methods to obtain type polymorphism. In general, polymorphic type systems with ∀ and ∃ quantifiers alone will tend to be inadequate for representing the results of a modular program analysis. Technically, this follows from the failure of these systems to satisfy a principal typings property (not to be confused with the much weaker property associated with Standard ML and related languages which is often called "principal types"). Type systems which obtain type polymorphism using only ∀ and ∃ quantifiers generally do not have principal typings; many such systems have been proven not to have principal typings. (For details, see Wells's ICALP '02 article.)

The Church Project's efforts in Compositional Analysis involve investigating the feasibility and real-world relevance of a new framework for modular program-analysis, which uses intersection and union types to support what is appropriately called finitary polymorphism (as opposed to the infinitary polymorphism supported by types quantified with ∀ and ∃). The starting point of this investigation is a recently designed polymorphic type system, called System I, for a foundational functional language, the λ-calculus. The chief feature of System I is the use of intersection types together with the new technology of expansion variables, which allows System I to satisfy a substitution-based principal-typings property. Although the resulting program analysis can be done in a fully modular manner, it is now restricted to a foundational language (the λ-calculus) missing many standard high-level programming features such as conditionals, recursive definitions, exceptions, assignments, input/output, etc. Considerable work — leading to extensions of the underlying λ-calculus, the syntax of types, and the typing rules — will be necessary in order to turn System I into a type system for a full-fledged programming language.

The Compositional Analysis effort aims at developing the theoretical foundations and conceptual tools for an efficient prototype implementation of a modular program-analyzer, based on appropriate extensions of System I. Such an implementation will be evaluated — or re-designed in parts or further extended — by the extent to which it will produce demonstrably better results in handling large software systems (enforcing larger classes of safety properties, statically detecting and ruling out larger classes of run-time errors). Foundational research will be pursued when it can contribute to resolving engineering issues.

Individual Participants

Adam Bakewell (Boston University)
Sebastien Carlier (Heriot-Watt University)
Joseph Hallett (Boston University)
Assaf Kfoury (Boston University)
Joe Wells (Heriot-Watt University)

Past Participants

Torben Amtoft (Kansas State University)
Gang Chen (Boston University)
Christian Haack (DePaul University)
Ori Schwartz (Boston University)
Geoff Washburn (University of Pennsylvania)

Software

Slide Presentations