Strong normalisation in the π-calculus

We introduce a typed π-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviour. The proof of strong normalisability combines methods from typed λ-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state, non-determinism, polymorphism, control and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply typed λ-calculus with products and sums and basic liveness in interaction. Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes.     

On the decidability of fragments of the asynchronous π-calculus

We study the decidability of a reachability problem for various fragments of the asynchronous π-calculus. We consider the combination of three main features: name generation, name mobility, and unbounded control. We show that the combination of name generation with either name mobility or unbounded control leads to an undecidable fragment. On the other hand, we prove that name generation without name mobility and with bounded control is decidable by reduction to the coverability problem for Petri Nets.     

On the Expressive Power of Polyadic Synchronisation in π-calculus

We extend the π-calculus with polyadic synchronisation, a generalisation of the communication mechanism which allows channel names to be composite. We show that this operator embeds nicely in the theory of π-calculus, and makes it possible to derive divergence-free encodings of distributed calculi. We give a separation result between the π-calculus with polyadic synchronisation (^eπ) and the original calculus, in the style of an analogous result given by Palamidessi for mixed choice. We encode Local Area π showing how to control the local use of resources in ^eπ.     

A semantic measure of the execution time in linear logic

We give a semantic account of the execution time (i.e. the number of cut elimination steps leading to the normal form) of an untyped MELL net. We first prove that: (1) a net is head-normalizable (i.e. normalizable at depth 0) if and only if its interpretation in the multiset based relational semantics is not empty and (2) a net is normalizable if and only if its exhaustive interpretation (a suitable restriction of its interpretation) is not empty. We then give a semantic measure of execution time: we prove that we can compute the number of cut elimination steps leading to a cut free normal form of the net obtained by connecting two cut free nets by means of a cut-link, from the interpretations of the two cut free nets. These results are inspired by similar ones obtained by the first author for the untyped lambda-calculus.     

There is no fully abstract fixpoint semantics for non-deterministic languages with infinite computations

It is well known that for many non-deterministic programming languages there is no continuous fully abstract fixpoint semantics. This is usually attributed to “problems with continuity”, that is, the assumption that the semantic functions should be continuous supposedly plays a role in the difficulties of giving a fully abstract fixpoint semantics. We show that for a large class of non-deterministic programming languages there is no fully abstract least fixpoint semantics even if one considers arbitrary functions (not necessarily continuous) over arbitrary partial orders (not necessarily complete).     

From algebraic semantics to denotational semantics for Verilog

This paper considers how the algebraic semantics for Verilog relates with its denotational semantics. Our approach is to derive the denotational semantics from the algebraic semantics. We first present the algebraic laws for Verilog. Every program can be expressed as a guarded choice that can model the execution of a program. In order to investigate the parallel expansion laws, a sequence is introduced, indicating which instantaneous action is due to which exact parallel component. A head normal form is defined for each program by using a locality sequence. We provide a strategy for deriving the denotational semantics based on head normal form. Using this strategy, the denotational semantics for every program can be calculated. Program equivalence can also be explored by using the derived denotational semantics. A short version of this paper appeared in Proc. ICECCS 2006: 11th IEEE International Conference on Engineering of Complex Computer Systems [48]. This work is partially supported by the National Basic Research Program of China (No. 2005CB321904), the National High Technology Research and Development Program of China (No. 2007AA010302) and the National Natural Science Foundation of China (No. 90718004). Jonathan Bowen is a visiting professor at King’s College London and an emeritus professor at London South Bank University.     

Objects in the π-Calculus

Two semantics for a parallel object-oriented programming language are presented. One is a two-level transitional semantics in which the global behaviour of a system is derived directly from the possible actions of its constituent objects. The other is by translation into the π-calculus. A close correspondence between the semantics is established.     

Call-by-name, call-by-value and the λ-calculus

This paper examines the old question of the relationship between ISWIM and the λ-calculus, using the distinction between call-by-value and call-by-name. It is held that the relationship should be mediated by a standardisation theorem. Since this leads to difficulties, a new λ-calculus is introduced whose standardisation theorem gives a good correspondence with ISWIM as given by the SECD machine, but without the letrec feature. Next a call-by-name variant of ISWIM is introduced which is in an analogous correspondence withthe usual λ-calculus. The relation between call-by-value and call-by-name is then studied by giving simulations of each language by the other and interpretations of each calculus in the other. These are obtained as another application of the continuation technique. Some emphasis is placed throughout on the notion of operational equality (or contextual equality). If terms can be proved equal in a calculus they are operationally equal in the corresponding language. Unfortunately, operational equality is not preserved by either of the simulations.     

Partial ordering models for concurrency can be defined operationally

Labelled rewriting systems are shown to be powerful enough for defining the semantics of concurrent systems in terms of partial orderings of events, even in the presence of non standard operators like N that is not expressible by means of concurrency and sequentialization. This contrasts with Pratt's claim.⁽¹⁾ The main operators proposed by Pratt are used here to construct terms denoting concurrent systems, the behavior of which consists of partially ordered multisets defined operationally.⁽²⁾ Fully abstractness of the denotational semantics as defined in Ref. 1 with respect to the operational one is finally proved.     

Can LCF be topped? Flat lattice models of typed λ-calculus

Plotkin ((1977) Theoret. Comput. Sci. 5: 223–256) examines the denotational semantics of PCF (essentially typed λ-calculus with arithmetic and looping). The standard Scott semantics V is computationally adequate but not fully abstract; with the addition of some parallel facilities, it becomes fully abstract, and with the addition of an existential operator, denotationally universal. We consider carrying out the same program for , the Scott models built from flat lattices rather than flat cpo's. Surprisingly, no computable extension of PCF can be denotationally universal; perfectly reasonable semantic values such as supremum and Plotkin's “parallel or” cannot be definable. There is an unenlightening fully abstract extension _A (approx), based on Gödel numbering and syntactic analysis. Unfortunately, this is the best we can do; operators defined by PCF-style rules cannot give a fully abstract language. (There is a natural and desirable property, operational extensionality, which prevents full abstraction with respect to .) However, we show that Plotkin's program can be carried out for a nonconfluent evaluator.     

On discrete lower π-strategies

Two-person zero-sum differential games of survival are investigated. It is assumed that player I, as well as player II, can employ during the course of the game any lower π-strategy [2], π(t_i) being a finite partition of [t₀, ∞). The concept of a discrete lower π-strategy is introduced and it is shown that if player I (II) confines himself to the space of discrete lower π-strategies, being a subset of the space of lower π-strategies, then he will be able to force the same lower (upper) value as if he could employ any lower π-strategy. Since we do not use any deep facts about differential games, the results contained here might be extended to continuous games.     

The μ-calculus as an assertion-language for fairness arguments

Various principles of proof have been proposed to reason about fairness. This paper addresses—for the first time—the question in what formalism such fairness arguments can be couched. To wit: we prove that Park's monotone first-order μ-calculus, augmented with constants for all recursive ordinals can serve as an assertion-language for proving fair termination of do-loops. In particular, the weakest precondition for fair termination of a loop w.r.t. some postcondition is definable in it. The relevance of this result to proving eventualities in the temporal logic formalism of Manna and Pnuelis (in “Foundations of Computer Science IV, Part 2,” Math. Centre Tracts, Vol. 159, Math. Centrum, Amsterdam, 1983) is discussed.     

A formalised first-order confluence proof for the λ-calculus using one-sorted variable names

We present the titular proof development that has been verified in Isabelle/HOL. As a first, the proof is conducted exclusively by the primitive proof principles of the standard syntax and of the considered reduction relations: the naive way, so to speak. Curiously, the Barendregt Variable Convention takes on a central technical role in the proof. We also show: (i) that our presentation of the λ-calculus coincides with Curry’s and Hindley’s when terms are considered equal up to α-equivalence and (ii) that the confluence properties of all considered systems are equivalent.     

A semantic characterization of the well-typed formulae of λ-calculus

A model-theoretic operation is characterized that preserves the property of being a model of typed λ-calculus (i.e., the result of applying it to a model of typed λ-calculus is another model of typed λ-calculus). An expression is well-typed iff the class of its models is closed under this operation.     

Dynamic Channel Screening in the Higher Order π-Calculus

Recently programming languages have been designed to support mobile code, i.e. higher-order code that is transferred from a remote location or domain and executed within the local environment. This may expose the internal interfaces and objects within a location to attacks by mobile code. In this work, we propose an extension of notations based on the Higher-Order π-calculus with primitive operators, called screening operators, whose role is to protect internal interfaces by dynamically restricting the visibility of channels. The usefulness of these operators is illustrated by applications involving resource access control. We show how restrictions on resource access control can be enforced dynamically in terms of screening operators, and contrast it with an alternative approach in which restrictions on the behaviour of processes are based on the notion of process type [17] and intended to be checked statically.     

Visualizing “typical” and “exotic” Internet traffic data

The threat of cyber attacks motivates the need to monitor Internet traffic data for potentially abnormal behavior. Due to the enormous volumes of such data, statistical process monitoring tools, such as those traditionally used on data in the product manufacturing arena, are inadequate. “Exotic” data may indicate a potential attack; detecting such data requires a characterization of “typical” data. We devise some new graphical displays, including a “skyline plot,” that permit ready visual identification of unusual Internet traffic patterns in “streaming” data, and use appropriate statistical measures to help identify potential cyberattacks. These methods are illustrated on a moderate-sized data set (135,605 records) collected at George Mason University.     

Synchronous and asynchronous handling of abnormal events in the μsystem

This paper presents a general model for dealing with abnormal events during program execution and describes how this model is implemented in the μSystem. (The μSystem is a library of C definitions that provide light-weight concurrency on uniprocessor and multiprocessor computers running the UNIX operating system.) Two different techniques can be used to deal with an abnormal event: an exception, which results in an exceptional change in control flow from the point of the abnormal event; and an intervention, which is a routine call from the point of the abnormal event that performs some corrective action. Users can define named exceptions and interventions in conjunction with ones defined by the μSystem. Exception handlers and intervention routines for dealing with abnormal events can be defined/installed at any point in a program. An exception or intervention can then be raised or called, passing data about the abnormal event and returning results for interventions. Interventions can also be activated in other tasks, like a UNIX signal. Such asynchronous interventions may interrupt a task's execution and invoke the specified intervention routine. Asynchronous interventions are found to be useful to get another task's attention when it is not listening through the synchronous communication mechanism.     

μC++: Concurrency in the object-oriented language C++

We present a design, including its motivation, for introducing concurrency into C++. The design work is based on a set of requirements and elementary execution properties that generate a corresponding set of programming language constructs needed to express concurrency. The new constructs continue to support object-oriented facilities such as inheritance and code reuse. Features that allow flexibility in accepting and subsequently postponing servicing of requests are provided. Currently, a major portion of the design is implemented, supporting concurrent programs on shared-memory uniprocessor and mulitprocessor computers.