[L3] _________________________ AMAST Links 01 03

Integrating Concurrent, Functional and Imperative

Programming Paradigms: Semantic Foundations

This PhD Thesis (University of Paris XI, Centre d'Orsay, defence date: July 1st 1994) is now available upon request from the author Dr. M. Debabi (Bull Corporate Research Center, Clayes-Sous-Bois, France). Also please notice that the thesis is written in French. For those interested in getting a copy, please send your request by e-mail to:

debabi@frcl.bull.fr

The aim of this work is to provide theoretical foundations for the unification of three paradigms. More accurately, the aim is to experiment with some ideas in an ML-like language extended with concurrency features. Thus, the language considered may be viewed as a sugared version of the call-by-value typed lambda-calculus that safely incorporates imperative and concurrent extensions. The language is polymorphic, implicitly typed and supports both functional and process abstractions. The language embodies a CSP-like process algebra which provides a set of concurrency combinators (internal choice, external choice, parallel composition and sequencing) used to compose expressions. A set of imperative aspects are also included in order to support mutable data.

To sum up, the main contributions are:

• A new typing discipline based on the reconstruction of principal types together with minimal side and communication effects.
• An extension of this discipline in order to cover declarations, patter-matching definitions, exceptions, etc.
• An operational semantics for a concurrent functional and imperative programming language.
• A denotational model for the above mentioned language, based on an accommodation of the acceptance trees model for handling communication, value-passing, assignment, return of results, dynamic creation of channels and processes, polymorphism and higher order objects.
• A semantic handling of the typing aspects and polymorphism at the dynamic level.
• A lifting of the static semantics as well as the two dynamic semantics to a CML core syntax.