[Prev][Next][Index][Thread]

Integrating concurrent, functional, and imperative programming


	I am pleased to announce the availability of my PhD thesis.
For those interested in getting a copy, please, let me know by *sending
an e-mail* to:

	debabi@frcl.bull.fr

	Please notice that the thesis is written in *French* according
to the requirements of Paris XI, Centre d'Orsay University. Please
find hereafter the details of the thesis.

-------------------------------------------------------------------------------

Title: 

       Integrating Concurrent, Functional and Imperative
       Programming Paradigms: Semantic Foundations.

Degree: 

       Ph.D. Thesis of  Universit\'e Paris XI, Centre d'Orsay.

Defence date: 

       July 1st 1994.

Laboratory: 

        Bull Corporate Research Center 
        (Clayes-Sous-Bois, France).

Abstract:

     	The intent of my Ph.D. work is to provide theoretical
foundations for the unification of three computational paradigms which
we refer to as concurrent, functional and imperative styles. More
accurately, the intention is to experiment our ideas on 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. Thus, the language is polymorphic, implicitly
typed and supports both functional and process abstractions. Functions
may be used to describe internal computations and expressions may
communicate by synchronized message passing over unidirectional typed
channels. 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.

     	The semantic theory presented in this work consists of a
static semantics of this language as well as two dynamic semantics.

     	The static semantics is inspired by the type and effect
discipline. More precisely, we present a generalization of this
discipline in order to deal with concurrency. The generalization
consists of an inference type system that propagates the communication
effects that results from channel creation, sending and receiving.
Hence a static evaluation of an expression in our type system yields
as a result, not only the principal type, but also all the minimal
side and communication effects.
	
     	The first dynamic semantics of the language is operational and
is inspired by the testing theory of Hennessy. It comes with an
operational preorder that induces a behavioral equivalence on
expressions.
 	
    	The second dynamic semantics presented is denotational. It is
based on an accommodation of the Hennessy's acceptance trees model.
It also may be viewed as a generalization of both RSL [R.E. Milne] and
VPLA [M. Hennessy & al.] models. The main novelties of the model
described in the thesis are its construction and its expressiveness.
The construction is not classical. In fact it is lead by the static
domains (types and effects) and the semantics of the language
constructs is expressed through dependent types. Hence a dependence
between the static and the dynamic semantics. The expressiveness of
the model is exemplified by the fact that it provides a semantics for
higher order processes integrating data, dynamic behaviors, process
and functional abstractions.

     	It should be noted that the two dynamic semantics take their
origin in De Nicola and Hennessy's work on CCS without $\tau$'s. This
work consists in providing a CCS semantics for CSP-like concurrency
combinators. A significant part in this semantic theory consists in
establishing that the static semantics is decidable and is coherent
with respect to the operational semantics.

	The last part of this semantic theory consists in lifting 
the semantic theory that we have elaborated to Concurrent ML (CML).
Thus we propose a static and a dynamic semantics for:


   o Implicit typing,
   o Polymorphism,
   o Exception handling,
   o Data structures defined by pattern matching,
   o Functional abstraction,
   o Concurrency synchronous primitives,
   o Imperative extensions,
   o Dynamic creation of references, channels and processes,
   o Reference, channel and process mobility.

	 This lifting generates some deviations from the theory
already presented. The main deviation consists in adopting a
continuation passing style in the denotational semantics in order to
keep the compositionality property of the semantics. This problem is
mainly due to the spawn operator of CML.

     To sum up, the main contributions of this dissertation are:

    o A new typing discipline based on the reconstruction of principal
      types together with  minimal side and communication effects.

    o An extension of this discipline in order to cover
      declarations, patter-matching definitions, exceptions, etc.
 
    o An operational semantics for a concurrent functional and 
      imperative programming language. 
	
    o 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.

    o A semantic handling of the typing aspects and polymorphism 
      at the dynamic level.
 
    o A lifting of the static semantics as well as the two dynamic
      semantics to a CML core syntax.




+-----------------------------------+----------------------------------+
|  Dr Mourad Debabi                 |                                  |
|                                   |  Tel: (33)-(1)-30 80 69 19       |
|  Bull Corporate Research Center   |                                  |
|  PC: B1/008,                      |  Fax: (33)-(1)-30 80 69 53       |
|  78340 Les Clayes-Sous-Bois,      |                                  |
|  France                           |  E-mail: debabi@frcl.bull.fr     |
+-----------------------------------+----------------------------------+