[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
<<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 [EMAIL PROTECTED] 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 [EMAIL PROTECTED] Please send a CV together with a description of your fields of expertise.