Constraints for Polymorphic Behaviours of Concurrent ML

Abstract

We present a type and behaviour reconstruction algorithm for Standard ML with concurrency. The behaviours express the communication effects during execution and resemble terms of a process algebra. The algorithm uses unification for the (essentially) free algebra of types and algebraic reconstruction for collecting constraints for the non-free algebra of behaviours. The algorithm and the statement and proof of soundness are designed so as to make no assumptions on the existence of ``principal´´ behaviours as these are unlikely to exist. The main complication in the development is that the notion of expansiveness does not suffice for a general treatment of the polymorphic let-construct.