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.