A Type-Based Algorithm for the Control-Flow
Analysis of Higher-Order Concurrent Programs
Mourad Debbabi, Ali Faour, Nadia Tawbi

Computer Science Department,
Laval University,
Quebec, G1K 7P4, Canada.
E-mails: {debabi,faour,tawbi}@ift.ulaval.ca

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.