Effect analysis for concurrent systems.

[10] develops a sound and complete type and behavior reconstruction algorithm for a fragment of Concurrent ML (CML), the starting point being the inference system presented by Hanne Riis Nielson and Flemming Nielson at POPL'94. The algorithm returns a set of constraints; and we show how to solve these in the monomorphic case (but not in general).

The monograph [1] gives an overview over type and effect systems, and then (improving upon the results of [33], [34] and [35]) develops an annotated type and effect system for a fragment of CML; the system uses constraints on the left hand side of the turn-stile and integrates Hindley-Milner polymorphism, subtyping, and effects. We show that the system is semantically sound; and develop a reconstruction algorithm that is sound and also complete. This algorithm has been used as the basis of a prototype implementation, available for experimentation on the WWW. [9] contains a description of the system, illustrated by several examples, as well as a brief account of the underlying theory. [25] shows that the system greatly assists in validating a number of safety properties for “realistic” concurrent systems.