Date: Tue, 23 Nov 1999 21:55:32 +0100
From: "Francisco J. Alberti"
Subject: CONFER II Workshop: Timetable
**********************************
** **
** CONFER II Workshop **
** **
** 25-26 November 1999 **
** **
** Paris **
** **
**********************************
(We apologise to those of you who are not supposed to receive this message)
Dear Participant:
Finally, I send you the preliminary timetable for the talks on Thursday and
Friday. We will give you a printed copy of the final schedule when you
register at the workshop.
The abstracts of some of the talks are collected together after the following
timetable.
================================================================================
THURSDAY 25
================================================================================
Morning:
9:00 - Registration
9:30 - Structured Coalgebras, SOS Specifications and Tiles for Open Systems
Ugo Montanari (Pisa)
(with Andrea Corradini, Pisa, and Reiko Heckel, Paderborn)
10:15 - Coffee Break
10:45 - The $\pi_F$-calculus: a $\pi$-calculus with fusions
Philippa Gardner (Cambridge)
(with Lucian Wischik)
11:30 - Assigning Types to Processes
Matthew Hennessy (Sussex)
(with Nobuko Yoshida)
12:15 - Lunch
Afternoon:
2:00 - Verifying arbitrary temporal formulas in the Temporal Logic of Actions
Lucian Wischik (Cambridge)
2:45 - Observational Equivalences for a Mobile Process Calculus
Asis Unyapoth (Cambridge)
3:30 - Coffee Break
4:00 - Secure Composition of Untrusted Code: Wrappers and Causality Types
Peter Sewell (Cambridge)
(with Jan Vitek, Purdue University)
4:45 - A Logical Framework for the spi calculus
Emilio Tuosto (Pisa)
================================================================================
FRIDAY 26
================================================================================
Morning:
9:30 - Double categories for calculi with name passing and name creation
Roberto Bruni (Pisa)
10:15 - Coffee Break
10:45 - A translation of Ambients in the distributed Join calculus
Alan Schmitt (INRIA)
11:30 - Authentication primitives and their compilation
Georges Gonthier (INRIA)
12:15 - Lunch
Afternoon:
2:00 - Closed Reductions in the Lambda Calculus
Ian Mackie (Paris)
2:45 - The lambda-sigma calculus enjoys finite normalisation cones
Paul-Andre Mellies (Paris)
3:30 - Coffee Break
4:00 - On the duality of call-by-name and call-by-value
Pierre-Louis Curien (Paris)
(with Hugo Herbelin)
4:45 - (Still available!)
================================================================================
Structured Coalgebras, SOS Specifications and Tiles for Open Systems
Ugo Montanari
(with Andrea Corradini, Pisa, and Reiko Heckel, Paderborn)
Structured coalgebras are coalgebras for an endofunctor on a category of
algebras, the latter defined by some equational specification. In the talk,
we consider two classes of transition systems with algebraic structure on
states. The first class is defined by using a quite general format of SOS
rules. The second class consists of certain monoidal double categories
called "tile models", which have been extensively employed to describe
distributed compositional systems. In both cases we present "decomposition"
properties which characterize when transition systems give rise to
structured coalgebras, in which case for instance bisimilarity becomes a
congruence.
Interestingly enough, when the two constructions are applied to the CCS
transition system, two different algebraic structures are exploited. In
particular, the tile version applies to "open CCS", a version of CCS with
free process variables.
For transition systems not satisfying the decomposition requirement, we
propose a closure construction which adds "context transitions", i.e.,
transitions that spontaneously embed states into contexts. The notion of
bisimilarity for the enriched system coincides with the notion of "dynamic
bisimilarity" for the original one, that is, with the coarsest bisimulation
which is a congruence. It is argued that dynamic bisimilarity is the
correct notion of bisimilarity for open systems.
================================================================================
The $\pi_F$-calculus: a $\pi$-calculus with fusions
Philippa Gardner
(with Lucian Wischik)
We introduce the $\pi_F$-calculus, a $\pi$-calculus with name fusion as
primitive. We provide embeddings of the $pi$-calculus, the $\pi_I$-calculus and
the fusion calculus in the $\pi_F$-calculus, and show the connection between a
bisimulation congruence for the $\pi$-calculus and the bisimulation congruence
arising from its translation in the $\pi_F$-calculus. We will also explain how
this work evolved from our recent work on process frameworks.
================================================================================
Assigning Types to Processes
Matthew Hennessy
(with Nobuko Yoshida)
In wide area distributed systems it is now common for
\emph{higher-order code} to be transferred from one domain to another;
the receiving host may initialise parameters and then execute the code
in its local environment. In this paper we propose a fine-grained
typing system for a higher-order $\pi$-calculus which can be used to
control the effect of such migrating code on local environments.
Processes may be assigned different types depending on their intended
use. This is contrast to most of the previous work on typing
processes where all processes are typed by a unique constant type,
indicating essentially that they are well-typed relative to a
particular environment. Our fine-grained typing facilitates the
management of access rights and provides host protection from
potentially malicious behaviour.
A process type is essentially an \emph{interface} limiting the
resources to which it has access, and the types at which they may be
used. Allowing resource names to appear both in process types and
process terms, as interaction ports, complicates the typing system
considerably. For the development of a coherent typing system, we use
a kinding technique, similar to that used by the system $F_{<:}$, and
order-theoretic properties of our subtyping relation.
Tecnical Report csr02/99 University of Sussex. Available from
http:\\www.cogs.sussex.ac.uk.
================================================================================
Verifying arbitrary temporal formulas in the Temporal Logic of Actions
Lucian Wischik
This talk describes how the TLC model-checker was extended to verify more
general temporal formulas. The formulas are converted into a disjunctive
normal form; they can then be solved using the tableau method of Clark and
Emerson [1981]. The technique was implemented during a summer internship at
Compaq Systems Research Center.
http://www.cl.cam.ac.uk/~ljw1004/academic/tlatalk/
================================================================================
Secure Composition of Untrusted Code: Wrappers and Causality Types
Peter Sewell
(with Jan Vitek, Purdue University)
The use of software components from untrusted or partially-trusted
sources is becoming common. A user would like to know, for example,
that they will not leak personal data to the net, but it is often
infeasible to verify that such components are well-behaved. Instead,
they must be executed in a secure environment, or _wrapper_, that
provides fine-grain control of the allowable interactions. In [1] we
introduced a process calculus with constrained interaction to express
wrappers and discussed their security properties. In this work we study
information flow properties of wrappers. We present a causal type
system that statically captures the allowed flows between wrapped
potentially badly-typed components; we use the type system to prove
that a non-trivial wrapper has the desired property.
================================================================================
A Logical Framework for the spi calculus
Emilio Tuosto
We provide a new LTS presentation of the spi calculus proving it
equivalent to the original presentation of the calculus.
Then we give a representation of the spi calculus in the Edimburg
Logical Framework.
This Logical Framework provide a setting to define formal
systems based on a general treatment of syntax, rules and
proofs by means of a typed lambda-calculus with dependent types.
Finally, we will prove that the LF-semantics and the
LTS-semantics are equivalent.
================================================================================
Double categories for calculi with name passing and name creation
Roberto Bruni
We introduce the notion of \emph{cartesian closed double category} to
provide mobile calculi for communicating systems with specific
semantic models: One dimension is dedicated to compose systems and
the other to compose their computations and their observations. Also,
inspired by the connection between simply typed $\lambda$-calculus
and cartesian closed categories, we define a new typed framework,
called \emph{double $\lambda$-notation}, which is able to express
the abstraction/application and pairing/projection operations in all
dimensions. In this development, we take the categorical presentation
as a guidance in the interpretation of the formalism. A case study of
the $\pi$-calculus, where the double $\lambda$-notation
straightforwardly handles name passing and creation, concludes the
presentation.
================================================================================
A translation of Ambients in the distributed Join calculus
Alan Schmitt
In this talk I describe the translation , which gives some
insight on the mechanisms hidden in ambient migrations. This translation was
proven correct and resulted in a distributed implementation of Ambients.
================================================================================
Closed Reductions in the Lambda Calculus
Ian Mackie
Closed reductions in the lambda-calculus is a strategy for a calculus
of explicit substitutions which overcomes many of the usual
syntactical problems of substitution. This is achieved by only moving
closed substitutions through certain constructs, which gives a weak
form of reduction, but is rich enough to capture the usual strategies
in the lambda-calculus (call-by-value, call-by-need, etc.) and is
adequate for the evaluation of programs. An interesting point is that
the calculus permits substitutions to move through abstractions, and
reductions are allowed under abstractions, if certain conditions hold.
The calculus naturally provides an efficient notion of reduction (with
a high degree of sharing), which can easily be implemented.