A Semantic Theory for Concurrent ML

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 al 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. 1 Motivation and Background We to provide theoretical foundations for Concurrent ML (CML) [25, 26]. CML can be vie...

• Type: Conference
• Year: 1994
• Where: TACS
• Authors: Dominique Bolignano, Mourad Debbabi
• Keywords: Concurrent ML, Denotational Model, Dynamic Semantic, Software Engineering, TACS 1994