[moca] PhD thesis: De la se'mantique des processus d'ordre supe'rieur

[Francesco Zappa Nardelli <Francesco.Zappa.Nardelli@xxxxxx>]

Dear all

I am pleased to announce that my PhD thesis "De la sémantique des
processus d'ordre supérieur" (On the Semantics of Higher-Order
Processes) is accessible at

    http://www.di.ens.fr/~zappa

It is written in English, and it includes an extended abstract in
French.

I hope you will find it of interest to you.  Comments are welcome.

Francesco Zappa Nardelli  (fz212@xxxxxxxxxxxx)

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

De la sémantique des processus d'ordre supérieur
(On the Semantics of Higher-Order Processes)

Summary: This PhD dissertation addresses the theories underlying the
mobile computation, with the aim to develop mathematical tools to
express and reason about mobile systems.

We studied the impact that mobility of active computations has on the
observational congruence, and in general on the equational theory of a
process language.  In particular, we focused on two process calculi,
namely the Seal Calculus and the Ambient Calculus, that offer two
opposite models of mobile computation.  In both cases, we found a
coinductive characterisation of observational congruence: these
results not only originate powerful proof methods to prove the
equivalence of two systems, but also highlight peculiarities of the
two models of mobility.  In the case of the Ambient Calculus, the
characterisation is complete: this important result required the
development of techniques to deal with asynchronous mobility and
``stuttering'' phenomena.  Also, we showed the soundness of up-to
proof techniques in the presence of higher-order computation.

We also studied presheaf categories as a general model of concurrency.
We gave an operational reading of a presheaf category suitable to
describe higher-order process and name generation.  This led us to a
compact but expressive language, called new-HOPLA, that directly
encodes a rich variety of process languages.  The language is typed,
and the type of a term describes the shape of the computation paths it
can perform.  The operational theory of the metalanguage has also been
developed, and the resulting operational equivalence theory has been
investigated.  The metalanguage has been used to give semantics to
rich process algebras like pi-calculus and Mobile Ambients.


  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html