Tech reports on Modules and Versioning, Applied Pi, Name-Passing

[These have respectively lots, a bit, and almost no types content... --p]

The technical reports

    Modules, Abstract Types, and Distributed Versioning
     Peter Sewell.  TR 506
    Applied Pi - A Brief Tutorial
     Peter Sewell.  TR 498

    Models for Name-Passing Processes: Interleaving and Causal
     Gian Luca Cattani and Peter Sewell.  TR 505
are available, either electronically from  

 and http://www.cl.cam.ac.uk/users/glc25/modnppictr.html

or, in hard copy, by emailing "tech-reports@cl.cam.ac.uk". Abstracts
are attached below.  Comments welcome.



Modules, Abstract Types, and Distributed Versioning. Peter Sewell.  TR 506

In a wide-area distributed system it is often impractical to 
synchronise software updates, so one must deal with many coexisting
versions.  We study static typing support for modular wide-area
programming, modelling separate compilation/linking and execution of
programs that interact along typed channels.  Interaction may involve
communication of values of abstract types; we provide the developer
with fine-grain versioning control of these types to support
interoperation of old and new code.  The system makes use of a
second-class module system with singleton kinds; we give a novel
operational semantics for separate compilation/linking and execution
and prove soundness.

Applied Pi - A Brief Tutorial.  Peter Sewell.  TR 498

This note provides a brief introduction to pi calculi and their
application to concurrent and distributed programming. Chapter 1
introduces a simple pi calculus and discusses the choice of
primitives, operational semantics (in terms of  reductions and of
indexed early labelled transitions), operational equivalences,
Pict-style programming and typing.  Chapter 2 goes on to discuss the
application of these ideas to distributed systems, looking informally
at the design of distributed pi calculi with grouping and interaction
primitives. Chapter 3 returns to typing, giving precise definitions
for a simple type system and soundness results for the labelled
transition semantics.  Finally, Chapters 4 and 5 provide a model
development of the metatheory, giving first an outline and then
detailed proofs of the results stated earlier.

Models for Name-Passing Processes: Interleaving and Causal
 Gian Luca Cattani and Peter Sewell.  TR 505

We study syntax-free models for name-passing processes. For
interleaving semantics, we identify the indexing structure 
required of an early labelled transition system to support the usual
pi-calculus operations, defining Indexed Labelled Transition 
Systems. For non-interleaving causal semantics we define Indexed
Labelled Asynchronous Transition Systems, smoothly generalizing both
our interleaving model and the standard Asynchronous Transition
Systems model for CCS-like calculi. In each case we relate a
denotational semantics to an operational view, for bisimulation and
causal bisimulation respectively. We establish completeness properties
of, and adjunctions between, categories of the two models. Alternative
indexing structures and possible applications are also
discussed. These are first steps towards a uniform understanding of
the semantics and operations of name-passing calculi.