![[Valid HTML 4.0!]](http://www.docs.uu.se/~victor/picts/vh40.gif){kind=small}
[an error occurred while processing this directive]
| Esprit WG-21836 |
CONFER-2 |
|||
The workshop dinner will be on Wednesday at 19.00 at Restaurant Movitz in Stockholm's Old Town. Address: Tyska Brinken 34, Subway station: Gamla Stan. The dinner will be paid individually (our CONFER2 funding is running short). Expect perhaps 300-400 SEK for this.
For abstracts, see below. (Each speaker has 40 minutes including discussion.)
| Time | Speaker | Title |
|---|---|---|
| Tuesday | ||
| 9.30 | Joachim Parrow | Welcome |
| Julian Rathke | A theory of bisimulation for a fragment of concurrent ML with local names | |
| Coffee/tea | ||
| Paul-Andre Mellies | Extensional Data Structures | |
| Vincent Danos | Disjunctive Tautologies as Synchronisation Schemes | |
| 12.00 | Lunch | |
| Jean-Francois Monin | A chat application written in Join calculus | |
| Cosimo Laneve | Inheritance in the join calculus | |
| Jean-Jacques Levy | Translating ambients into the Join Calculus | |
| 15.00 | Coffee/tea | |
| Peter Sewell | Models for name passing processes: interleaving and causal | |
| Mads Dam | Proof systems for pi-calculus logics | |
| 17.00 | End | |
| Wednesday | ||
| 9.30 | Business meeting | |
| Fabio Gadducci | Term graph rewriting and the pi-calculus | |
| Coffee/tea | ||
| José-Luis Vivas | A process calculus with dynamic binding of names | |
| Jan Willem Klop | Proof systems for cyclic term graphs | |
| 12.30 | Lunch | |
| Roberto Amadio | On the reachability problem in cryptographic protocols | |
| Sylvain Conchon | Type systems and security | |
| Björn Victor | Towards automatic verification of security protocols | |
| 19.00 | Workshop dinner | |
| Speaker | Title | Abstract |
|---|---|---|
| Paul-Andre Mellies | Extensional Data Structures | about game and denotational semantics of PCF-sequentiality. |
| Roberto Amadio | On the reachability problem in cryptographic protocols | |
| Julian Rathke | A theory of bisimulation for a fragment of concurrent ML with local names | |
| Concurrent ML is an extension of Standard ML with pi-calculus-like primitives for multi-threaded programming. CML has a reduction semantics, but to date there has been no labelled transitions semantics provided for the entire language. In this paper, we present a labelled transition semantics for a fragment of CML which includes features not covered before: dynamically generated local channels and thread identifiers. We show that weak bisimulation for this sublanguage is a congruence, and coincides with barbed bisimulation congruence. We also provide a variant of Sangiorgi's normal bisimulation and show that this too coincides with bisimulation. | ||
| Jean-Francois Monin | A chat application written in Join calculus | |
|
The talk will report the current status of our first experiment on
writing a telecom application with join-calculus, as implemented in
JoCaml. It is an attempt to write in a concise way an IRC (Internet
Relay Chat) application.
IRC provides a way of communicating in real time with other users over a net of machines. Each user runs a program (called a "client") to connect to an IRC server. The server relays information to and from other servers on the same net. Real life IRC consists of various separate world wide networks. The largest ones are EFnet (the original IRC net, often having more than 32,000 people at once), Undernet, IRCnet, DALnet, and NewNet. Our application is currently only a toy IRC dedicated to the experimentation of concepts. We are especially interested in the advantages of mobile code we can take for :
| ||
| Vincent Danos | Disjunctive Tautologies as Synchronisation Schemes | |
| In the ambient logic of classical second order propositional calculus, we solve the specification problem for a family of excluded middle like tautologies. These are shown to be realized by sequential simulations of specific communication schemes for which they provide a safe typing mechanism. | ||
| Cosimo Laneve | Inheritance in the join calculus | |
| We propose an object-oriented calculus with internal concurrency and class-based inheritance that is built upon a process calculus---the join calculus.
In our calculus, method calls, locks, and states are handled in a uniform manner, using labeled messages. Classes are partial definitions that can be combined and transformed. We design operators for behavioral and synchronization inheritance, and we give a type system that statically enforces basic safety properties. Our approach to inheritance and synchronization is compatible with the present JoCaml implementation of the join calculus. | ||
| Sylvain Conchon | Type systems and security | |
| Jean-Jacques Levy | Translating ambients into the Join Calculus | |
| Björn Victor | Towards automatic verification of security protocols | Decidability and symbolic semantics of spi-calculus |
| Jan Willem Klop | Proof systems for cyclic term graphs | |
| Cyclic term graphs are important in functional programming and have also other applications such as recursive types. We discuss and compare two complete proof systems, one being the usual 'folklore' system based on a fixed point rule, and one based on a coinductive proof rule due to Brandt and Henglein. | ||
| Mads Dam | Proof systems for pi-calculus logics | |
| In this paper we study the problem of verifying general temporal and functional properties of mobile and dynamic process networks, cast in terms of the pi-calculus. Much of the expressive power of this calculus derives from the combination of name generation and communication (to handle mobility) with dynamic process creation. In the paper we introduce an extension of the modal mu-calculus with name equality, inequality, first-order universal and existential quantification, and primitives for name input and output as an appropriate temporal logic for the pi-calculus. A compositional proof system is given with the scope of verifying dynamic networks of pi-calculus agents against properties specified in this logic. The proof system is shown to be sound in general and complete for the modal fragment of the specification logic. Milner's encoding of data types into the pi-calculus provide an interesting application study, since the encodings make essential use of all the distinguishing features of the pi-calculus, including dynamic process creation. We give two examples. First we suggest an encoding of the type of natural numbers and demonstrate how the proof system can be used to formally establish type correctness properties. Secondly we show how the proof system can be used to uniformly prove properties of chained buffers. | ||
| José-Luis Vivas | A process calculus with dynamic binding of names | |
| We propose a notation inspired on the reflexive chemical abstract machine. We preserve reflexion but eliminate locality, and add operators that support the notions of dynamic binding, environment, module, and object structuring concepts in general. | ||
| Peter Sewell | Models for name passing processes: interleaving and causal | |
| I will be talking about joint work with Gian Luca Cattani on syntax-free models of name-passing processes. I will begin by reviewing some of the reasons which led Luca and I to look into this problem. In particular I will show by examples the reasons why standard models of concurrency such as Labelled Transition Systems are not appropriate for modelling pi-terms. The same set of examples will motivate the definition of the new models that we introduce: Indexed Labelled Transition Systems (ILTS). A compositional semantics of pi-terms as ILTSs will be defined and a few simple categorical properties, which allow for the interpretation of recursive processes, established. Causality is then built into the models by adding events and an independence relation between them, leading to the notion of Indexed Asynchronous Transition System (IATS). A compositional semantics of pi-terms as IATSs is deduced and bisimulation in the model related to Boreale and Sangiorgi's Causal Bisimulation. Time permitting I will end up with a short discussion on indexing structures alternative to the one we chose and possibly with some more (easy) general non-sense to formally relate the two categories of models to each other. | ||
| Fabio Gadducci | Term graph rewriting and the pi-calculus | |
| We present a graphical implementation for processes of the finite pi-calculus, where each process is encoded into a suitable term graph. Our implementation is sound and complete with respect to the standard structural congruence between processes, in the sense that equivalent processes are mapped into isomorphic term graphs. In addition, we show how these properties of the encoding allow for the use of a standard graph rewriting mechanism for simulating the reduction semantics for pi-calculus. | ||
| Name | Site |
|---|---|
| Cosimo Laneve | Bologna |
| Vincent Danos | ENS |
| François Maurel | ENS |
| Paul-André Mellies | ENS |
| Roberto Amadio | Provence |
| Julian Rathke | Sussex |
| Massimo Merro | Sussex |
| Pascal Brisset | France Telecom |
| Didier Begay | France Telecom |
| Jean-François Monin | France Telecom |
| Bent Thomsen | ICL |
| Lone Leth Thomsen | ICL |
| Uwe Nestmann | Aalborg |
| Peter Sewell | Cambridge |
| Pawel Wojciechowski | Cambridge |
| Lucian Wischik | Cambridge |
| Alistair Turnbull | Cambridge |
| Philippa Gardner | Cambridge |
| Jean-Jacques Levy | Rocquencourt |
| Fabrice Le Fessant | Rocquencourt |
| Sylvain Conchon | Rocquencourt |
| Jan Willem Klop | CWI |
| Fabio Gadducci | Pisa |
| Joachim Parrow | KTH |
| Mads Dam | KTH |
| José-Luis Vivas | KTH |
| Björn Victor | Uppsala |
| Björn Victor Last modified: Thu, 22-Jun-2000 09:02 MEST |
[an error occurred while processing this directive]
[an error occurred while processing this directive]
|