Type and Behaviour Reconstruction for Higher-Order Concurrent Programs

Torben Amtoft
Flemming Nielson
Hanne Riis Nielson

In 6th NWPT, pages 80-95

Abstract:

In this paper we develop a sound and complete type and behaviour inference algorithm for a fragment of CML (Standard ML with primitives for concurrency). Behaviours resemble terms of a process algebra and yield a concise presentation of the communications taking place during execution; types are mostly as usual except that function types and ``delayed communication types'' are labelled by behaviours expressing the communications that will eventually take place. The development of the present paper improves a previously published algorithm in not only achieving a sound algorithm for type inference but also one that is complete, due to an alternative strategy for generalising over types and behaviours. Although we show how to solve special kinds of constraints the problem of a general solution procedure for the constraints generated remains; this is related to an open problem concerning whether all programs typable in Standard ML (with concurrency primitives) are also typable in our system.

Comments
{tamtoft,fn,hrn}@daimi.aau.dk.

Available as PostScript, DVI.

BRICS WWW home page