[TYPES/announce] postdoc position available at ENS Lyon

[Daniel.Hirschkoff@ens-lyon.fr]

<<work in the position offered below may focus on type systems for
analysis of concurrent systems>>



The Plume team of the Ecole Normale Superieure de Lyon
(http://www.ens-lyon.fr/LIP/PLUME/plume.us.html) is offering a 12
month job to collaborate within the project MoDyFiable ("Modularite
Dynamique Fiable").


The goal of this project is to provide a core programming model for
dynamic modularity. By dynamic modularity, we refer to the ability in
modern software to act on the structure of a system at runtime
(deployment, dynamic update, code mobility, ..). In collaboration with
INRIA project SARDES (Grenoble -- France), we are currently developing
a process algebraic model where to represent and analyse such
phenomena. Below is a succinct description of the main subjects
related to this project.



Central to our model is the mechanism of passivation, which allows one
to transform a running computation unit into some passive entity, that
can be modified, or shipped in a message. The interplay between
passivation and other typical notions of distributed computation (such
as logical vs. physical localities, distant communication,
encapsulation, ..) raises important and interesting questions from
several points of view:

1 - Programming language: implementation, high level constructs, type
systems.

Many design choices arise when trying to implement passivation in the
setting of a distributed computation. We study these by defining and
analysing abstract machines for the distributed execution of our
process models.  Additionally, we work on understanding how our core
calculus can be extended in order to provide useful and expressive
primitives to program dynamic modularity.  We would also like to
develop type systems for encapsulation or resource access control.


2 - Models: behavioural equivalences, semantic models.

In presence of named localities and passivation, most of the
behavioural laws that hold in usual process calculi fail.  We are
working on understanding what notion of behavioural equivalence is
provided in a calculus with passivation, and what (coinductive) proof
techniques can be defined to help establishing equivalences.

There are many ways to include passivation in a core formal model for
concurrent computation, and we lack means to compare these. General
frameworks like Milner's Bigraphs should help us in relating various
proposals and providing an abstract understanding of passivation.
Alternatively, we would like to understand using category theory the
properties we want to guarantee for the models we are currently
developing. 




Relevant references to learn more about the models we study include
the following:

- Alan Schmitt, Jean-Bernard Stefani: The m-calculus: a higher-order
  distributed process calculus. POPL 2003: 50-61
- Philippe Bidinger, Alan Schmitt, Jean-Bernard Stefani: An Abstract
  Machine for the Kell Calculus. FMOODS 2005: 31-46 
- Daniel Hirschkoff, Tom Hirschowitz, Damien Pous, Alan Schmitt,
  Jean-Bernard Stefani: Component-Oriented Programming with Sharing:
  Containment is Not Ownership. GPCE 2005: 389-404 

More recent, unpublished, developments of our models are available
upon request. More generally, interested candidates can get in contact
with Daniel.Hirschkoff at ens-lyon.fr for further information.



** To apply **

The candidate should have a good knowledge of process algebras for
concurrency (CCS, the pi-calculus). Further specialisation along one
of the aforementioned research directions would be appreciated. A PhD
is mandatory in order to apply.



The job is available immediately (spring 2007), but can also start
later in 2007 (until september 2007). The salary is 2150 euros per
month "brut" (which includes social insurance -- take out something
like 15-20% to obtain the actual income every month).

Candidates should get in contact with Daniel.Hirschkoff at ens-lyon.fr.
Please send a CV together with a description of your fields of
expertise.