Calculi for Concurrent Processes

InmytalkIsurveyedsomeofthemainstreamresearchthathasbeendoneintheareaofprocesscalculiduringthelasttwentyyears-thoughfocusingonsomelastdevelopments,regardingespeciallymobilecomputing.IstartedwithabriefaccountofthepioneeringworkofMimerandhisco-workersonCCS,theCalculusofCommunicatingSystems.ThisbeguninthelateseventieswhenMimerrealizedthatScott'sdenotationalsemanticswasnotsofruitfulconcerningconcurrency.ApreliminarystepwastakenbyMilnerwithhisflowalgebra,consistingofasmallsetofoperationsandaxiom…     

Typing termination in a higher-order concurrent imperative language

We propose means to predict termination in a higher-order imperative and concurrent language à la ML. We follow and adapt the classical method for proving termination in typed formalisms, namely the realizability technique. There is a specific difficulty with higher-order state, which is that one cannot define a realizability interpretation simply by induction on types, because applying a function may have side-effects at types not smaller than the type of the function. Moreover, such higher-order side-effects may give rise to computations that diverge without resorting to explicit recursion. We overcome these difficulties by introducing a type and effect system for our language that enforces a stratification of the memory. The stratification prevents the circularities in the memory that may cause divergence, and allows us to define a realizability interpretation of the types and effects, which we then use to establish that typable sequential programs in our system are guaranteed to terminate, unless they use explicit recursion in a divergent way. We actually prove a more general fairness property, that is, any typable thread yields the scheduler after some finite computation. Our realizability interpretation also copes with dynamic thread creation.     

The π-Calculus in Direct Style

We introduce a calculus which is a direct extension of both the and the calculi. We give a simple type system for it, that encompasses both Curry's type inference for the -calculus, and Milner's sorting for the -calculus as particular cases of typing. We observe that the various continuation passing style transformations for -terms, written in our calculus, actually correspond to encodings already given by Milner and others for evaluation strategies of -terms into the -calculus. Furthermore, the associated sortings correspond to well-known double negation translations on types. Finally we provide an adequate CPS transform from our calculus to the -calculus. This shows that the latter may be regarded as an assembly language, while our calculus seems to provide a better programming notation for higher-order concurrency. We conclude by discussing some alternative design decisions.     

Algèbre de processus et synchronisation

We introduce here a calculus of processes, involving an asynchronous parallel composition and some synchronization primitives. It is shown that, in this calculus, many synchronization mechanisms can be formulated; in fact, this calculus is equivalent to Milner's synchronous calculus (1980, 1983). We evaluate its expressive power by means of languages of behaviours.     

A theory of processes with localities

We study a notion of observation for concurrent processes which allows the observer to see the distributed nature of processes, giving explicit names for the location of actions. A general notion of bisimulation related to this observation of distributed systems is introduced. Our main result is that these bisimulation relations, particularized to a process algebra extending CCS, are completely axiomatizable. We discuss in detail two instances of location bisimulations, namely the location equivalence and the location preorder.This work has been partly supported by the ESPRIT/BRA project CEDISYS.