We design a mutex library for Hop -- a dialect of Scheme which supports preemptive multithreading and shared memory -- that mixes deadlock prevention and deadlock avoidance to provide an easy to use, expressive, and safe locking function. This requires an operation to acquire several mutexes simultaneously, for which we provide a starvation-free algorithm. Choosing a formal definition of starvation-freedom leads us to identify the concept of asymptotic deadlock. Preliminary observations seem to show that our library has negligible impact on the performance of real-life applications. Our work could be applied to other languages such as Java.

We propose a small-step operational semantics to support reasoning about Web applications written in the multitier language HOP. The semantics covers both server side and client side computations, as well as their interactions, and includes creation of Web services, distributed client-server communications, concurrent evaluation of service requests at server side, elaboration of HTML documents, DOM operations, evaluation of script nodes in HTML documents and actions from HTML pages at client side. We also model the browser same origin policy (SOP) in the semantics. We propose a safety property by which programs do not get stuck due to a violation of the SOP and a type system to enforce it.

Memory models define an interface between programs written in some language and their implementation, determining which behaviour the memory (and thus a program) is allowed to have in a given model. A minimal guarantee memory models should provide to the programmer is that well-synchronized, that is, data-race free code has a standard semantics. Traditionally, memory models are defined axiomatically, setting constraints on the order in which memory operations are allowed to occur, and the programming language semantics is implicit as determining some of these constraints. In this work we propose a new approach to formalizing a memory model in which the model itself is part of a weak operational semantics for a (possibly concurrent) programming language. We formalize in this way a model that allows write operations to the store to be buffered. This enables us to derive the ordering constraints from the weak semantics of programs, and to prove, at the programming language level, that the weak semantics implements the usual interleaving semantics for data-race free programs, hence in particular that it implements the usual semantics for sequential code.

We address the issue of declassification in a language-based security approach. We introduce, in a Core ML-like language with concurrent threads, a declassification mechanism that takes the form of a local flow policy declaration. The computation in

We address the issue of declassification in a language-based security approach. We introduce, in a Core ML-like language with concurrent threads, a declassification mechanism that takes the form of a local flow policy declaration. The computation in the scope of such a declaration is allowed to implement information flow according to the local policy. This dynamic view of information flow policies is supported by a concrete presentation of the security lattice, where the confidentiality levels are sets of principals, similar to access control lists. To take into account declassification, and more generally dynamic flow policies, we introduce a generalization of non-interference, that we call the non-disclosure policy, and we design a type and effect system for our language that enforces this policy.

In a call-by-value language, representing objects as recursive records requires using an unsafe fixpoint. We design, for a core language including extensible records, a type system which rules out unsafe recursion and still supports the construction of a principal type for each typable term. We illustrate the expressive power of this language with respect to object-oriented programming by introducing a sub-language for “mixin-based” programming.

We study an asynchronous distributed π-calculus, with constructs for localities and migration. We show that a static analysis ensures the receptiveness of channel names, which, together with a simple type system, guarantees the message deliverability property. This property states that any migrating message will find an appropriate receiver at its destination locality. We argue that this distributed, receptive calculus is still expressive enough while allowing for an effective type inference à la ML.

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.

Abstract 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.

We introduce a new kind of abstract machine based on the chemical metaphor used in the Γ language of Banâtre & al. States of a machine are chemical solutions where floating molecules can interact according to reaction rules. Solutions can be stratified by encapsulating subsolutions within membranes that force reactions to occur locally. We illustrate the use of this model by describing the operational semantics of the TCCS and CCS process calculi. We also show how to extract a higher-order concurrent λ-calculus out of the basic concepts of the chemical abstract machine.