[Prev][Next][Index][Thread]
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
http://www.cl.cam.ac.uk/users/pes20/
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.
Peter
-------
Modules, Abstract Types, and Distributed Versioning. Peter Sewell. TR 506
Abstract:
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
Abstract:
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
Abstract:
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.