A semantic theory for concurrent ML

Abstract

In this paper we present a semantic theory for Concurrent ML. It consists of a new effect-based type system and a denotational model. The new type system is based on an extension of the type and effect discipline. In addition to the automatic reconstruction of usual principal types, it computes also the minimal communication effects. The dynamic semantics developed in this paper is denotational. It is based on an accommodation of the Hennessy’s acceptance-trees model for handling polymorphism, communication, value-passing, process and functional abstractions and higher order objects. In order to avoid some limitations due to the domain theory, the denotational model is made dependent on the static semantics. Hence, the dynamic domains are typed by the static values. The dynamic semantic evaluation of CML constructs is then expressed using dependent types in the meta-language.