A type based algorithm for the control flow analysis of higher order concurrent programs

Abstract

We address, in a type-based framework, the problem of control-flow analysis for concurrent and functional languages. We present an efficient algorithm that propagates automatically types, communica-tion effects and call graphs. The algorithm comes with a logical char-acterization that consists of a type proof system. The latter operates on a Concurrent ML core-syntax: a strongly typed, polymorphic kernel that supports higher-order functions and concurrency primitives. Effects are represented as algebraic terms that record communication effects re-sulting from channel creation, sending and receiving. Call graphs record function calls and are captured by a term algebra that is close to usual process algebras. Types are annotated with effects and call graphs. For the sake of flexibility, a subtyping relation is considered on the type al-gebra. We present the language syntax together with its static semantics that consists of the typing rules and an inference algorithm. The latter is proved to be sound with respect to the typing rules.