The INI has a new website!

This is a legacy webpage. Please visit the new site to ensure you are seeing up to date information.

Isaac Newton Institute for Mathematical Sciences

Semantics of Computation

1 July - 31 December 1995

Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)

High-level Concurrent Languages: Foundations and Verification Techniques

Schedule

Monday

Tuesday

Wednesday

Monadic types for the semantics of concurrent functional programming

Alan Jeffrey

This talk presents a concurrent functional programming language based on Reppy's CML, but with a type system based on Moggi's computational monads. The operational semantics for the language is presented, and compared with the semantics of a subset of CML.

Idioms for Interaction

Kohei Honda

In imperative programming languages we started from hacking in machine languages and then assembly languages, which was hard but rewarding: later we arrived at high-level language constructs on the basis of, and reflecting on, those experiences, making programming much easier and more disciplined. Similarly in functional programming languages, we started with the pure lambda calculus and later reached the present-day highly polished typed programming languages. In another tradition, the advancement from the pure lisp to varied lisp-based languages may be seen in the same way.

Well, how about high-level constructs for concurrent programming languages? In the present talk, the speaker suggests that a similar story can be told starting from hacking in pi-calculus and its descendants. We show how various high-level "idioms for interaction" naturally arise if you persevere in encoding various non-trivial computational entities in those calculi, keeping eyes on the underlying abstract structures. We may also be able to discuss type principles which give disciplined ways of combining these idioms to form a process with desired behaviour.

The talk is thus an invitation to the hacking in pi-calculus and its descendants (you can even hack with its combinators!), by which we may arrive at languages constructs with higher-level abstraction, and which, by the way, itself is a fun to do.

Functional Computation in a Uniformly Concurrent Calculus with Logic Variables

We present the $\delta$-calculus, a model of uniformly concurrent computation. It integrates eager and lazy functional computation and describes the intended complexity behavior in both cases.

We call concurrent computation {\sl uniformly concurrent}, if result, termination and complexity are independent from the computation order. We establish theses properties for the $\delta$-calculus by proving its uniform confluence.

The $\delta$-calculus extends to models of concurrent computation providing for consumable resources and indeterminism. Such are the $\gamma$-calculus, a foundation of concurrent computation with constraints, and the $\pi$-calculus, a successor of CCS based on channel communication.

The $\delta$-calculus is a relational calculus with procedural abstraction and application. It provides for communication over logic variables and for suspension on their instantiation. Both mechanisms come naturally with parallel composition and declaration.

We embed the eager and the lazy $\lambda$-calculus into the $\delta$-calculus. Using explicit references we guarantee that functional arguments are evaluated at most once. Explicit references are a special form of logic variables. These are needed too for representing lazy functional control. We prove the adequacy of the embedding of the eager $\lambda$-calculus with respect to termination and complexity. We conjecture that the embedding of the lazy $\lambda$-calculus preserves termination and improves complexity.

"Non-interleaving semantics for mobile processes"

Corrado Priami

It is a joint work with Pierpaolo Degano. Its abstract follows:

The paper studies causality in $\pi$-calculus. Our notion of causality combines the dependencies given by the syntactic structure of processes with those originated by passing names. Our studies show that two transitions not causally related may however occur in a fixed ordering in any computation, i.e., $\pi$-calculus may implicitly express a precedence between actions. Our causality relation still induces the same partial order of transitions for all the computations that are obtained by shuffling transitions that are concurrent (i.e. related neither by causality nor by precedence). Other non-interleaving semantics are investigated and compared. The presentation takes advantage from a parametric definition of process behaviour given in an $SOS$ style. All the results on bisimulation-based equivalences, congruences, axiomatizations and logics are taken (almost) without modifications from the interleaving theory. Finally, we extend our approach to higher-order $\pi$-calculus, enriched with a {\em spawn} operation.

An extension of the above theory to full Facile is under development. Some hints on the new work can be supplied, if appropriate.

Functional Computation in a Uniformly Concurrent Calculus with Logic Variables

Joachim Niehren

We present the $\delta$-calculus, a model of uniformly concurrent computation. It integrates eager and lazy functional computation and describes the intended complexity behavior in both cases.

We call concurrent computation {\sl uniformly concurrent}, if result, termination and complexity are independent from the computation order. We establish theses properties for the $\delta$-calculus by proving its uniform confluence.

The $\delta$-calculus extends to models of concurrent computation providing for consumable resources and indeterminism. Such are the $\gamma$-calculus, a foundation of concurrent computation with constraints, and the $\pi$-calculus, a successor of CCS based on channel communication.

The $\delta$-calculus is a relational calculus with procedural abstraction and application. It provides for communication over logic variables and for suspension on their instantiation. Both mechanisms come naturally with parallel composition and declaration.

We embed the eager and the lazy $\lambda$-calculus into the $\delta$-calculus. Using explicit references we guarantee that functional arguments are evaluated at most once. Explicit references are a special form of logic variables. These are needed too for representing lazy functional control. We prove the adequacy of the embedding of the eager $\lambda$-calculus with respect to termination and complexity. We conjecture that the embedding of the lazy $\lambda$-calculus preserves termination and improves complexity.

The Weak Late pi-calculus Semantics as Observation Equivalence

by GianLuigi Ferrari, Ugo Montanari and Paola Quaglia

We show that the Weak Late pi-calculus semantics can be characterized as ordinary Observation congruence over a specialized transition system where both the instantiation of input placeholders and the name substitutions, due e.g. to communication, are explicitly handled via suitable constructors.

The approach presented here generalizes the one proposed in a previous paper. The pi-calculus transitional semantics is reduced to a SOS framework fitting with a mild generalization of the De Simone format, and we retrieve a complete axiomatization of the Strong Late semantics by turning rules into equations.

The Weak Late pi-calculus semantics is then axiomatized by simply adding Milner's tau-laws to the proof system for the Strong equivalence. Up-to-date, the Weak Late pi-calculus bisimulation was only characterized relying on the notion of Symbolic bisimulation.

Resorting to Observation equivalence provides a framework which is general enough to allow to recover, in straightforward ways, other bisimulation semantics (e.g. Early, both Strong and Weak, and Dynamic and Branching, both Early and Late).

Checking Bisimilarity for Finitary pi-calculus

by Ugo Montanari and Marco Pistore

In this paper we associate to every pi-calculus agent an "irredundant unfolding", i.e. a labeled transition system equipped with the ordinary notion of strong bisimilarity, so that early strongly bisimilar agents are mapped into strongly bisimilar unfoldings.

For a class of finitary agents (that strictly contains the finite control agents) without matching, the corresponding unfoldings are finite and can be built efficiently. The main consequence of the results presented in the paper is that the irredundant unfolding can be constructed also for a single agent, and then a minimal realization can be derived from it employing the ordinary partition refinement algorithm. Instead, according to previous results only pairs of pi agents could be unfolded and tested for bisimilarity, and no minimization of a single agent was possible. In addition, the complexity bounds are in our case remarkably better when comparable, and the applicability is broader (finitary agents instead of finite control agents).

Copyright © Isaac Newton Institute