Interaction and Space, Logics and Concurrency
Marseille - Luminy
February 27 - March 3, 2006
Organizers:
Etienne Lozes,
Daniel Hirschkoff.
Context: This workshop is part of Geometry of Computation 2006 (
Geocal06), a special series of
events in theoretical computer science organized by the
GEOCAL group and taking
place at the
CIRM from January 30 to
March 3. Geocal06 is supported by the following institutions:
IML,
FRUMAM,
Luminy,
UnivMed,
Genopole,
CIRM,
CNRS.
The aim of this workshop is to bring together people interested in the interplay between research on algebraic models for mobile and distributed computing, where one can describe and reason about the spatial structure and interaction possibilities of processes, and recent developments in proof theory, notably in ludics, where similar mechanisms show up.
In models like the pi-calculus or mobile ambients, a process configuration is described as a collection of agents that can interact via appropriate mechanisms (named channels, locations, interaction capabilities). Structure-sensitive relations between processes have been proposed to reason about mobility and locality properties of a system. Among these, the so-called spatial logics extend existing modal logics to specify the actual structure of a process and its evolution along computation.
In logic, the central mechanism of cut-elimination has been presented recently in a way that bears striking analogies with a concurrent scenario. In ludics, in particular, loci, which correspond to formula occurrences, are the places where cut happens, in an interactive fashion. Similarly, denotational models based on games exploit the notion of synchronization trees generated by interacting players.
Actual connections between denotational semantics or logic and concurrency exist, notably on the study of the proof theory of spatial logics, and on process-algebra based models of linear logic. The goal of this meeting is to investigate further the possible interactions between these areas, and to find out whether such analogies can lead to profound connections, or, at least, if methods and results on one side can provide inspiration for the other side.
|
9h - 10h30 |
11h - 12h30 |
14h - 15h30 |
16h - 17h30 |
| Mon 27 |
Logics in concurrency
|
Logics in concurrency
|
|
|
| Tue 28 |
|
|
Reasoning on resources
|
Reasoning on resources
|
| Thu 2 |
Spatial verification
|
Spatial verification
|
Logics in concurrency
|
Resources/Verification
|
| Fri 3 |
|
|
|
|
-
Emmanuel Beffara
,
PPS, Paris
Title Concurrent realisability
Abstract
In this talk, I will present a logician's approach to the study of
concurrent processes. We start from a variant of polyadic pi-calculus,
equipped with a parametrable kind of observation (divergence, may or
must testing...), from which we deduce an abstract notion of behaviour.
The structure of behaviours leads to the definition of logical
connectives, inspired by spatial or temporal logics, that describe the
fundamental properties of process interaction. The logical system we
obtain is a form of linear logic that provides a new typing system for
processes that guarantees good properties, like non-divergence and
deadlock-freeness. The type system also establishes a meaningful
proof/program correspondence for linear logic that integrates well with
previous studies on the decomposition of functional computation into
process calculi.
-
Giovanni Conforti
,
Pisa
Title BiLog : a spatial logic framework
Abstract
Bigraphs are emerging as an interesting model for concurrent calculi, like pi-calculus, ambient calculus and petri-nets. Bigraphs are built orthogonally on two structures: a hierarchical place graph for locations and a link (hyper-)graph for connections. Inspired from the bigraphical structure we introduce a new spatial logic framework able to express all the static spatial logic introduced so far. We then observe how the relatively simple generalization of spatial logics become more subtle in presence of dynamic in the model and modal temporal operators in the logic. In particular we observe that in some cases is possible to express a form of next step modality in a completely static framework. We also explore the notion of transparency/opaqueness of constructors and their influence in the logic.
-
Matthew Collinson
,
Bath University
Title Bunched and Multiplicative Polymorphism, Regions and Locations
Abstract
The Logic of Bunched Implications, BI, has proved to be of great interest
and to have many applications in computer science, for example to
Separation Logic. I will describe extensions of BI to second-order.
A second-order lambda calculus with both additive and multiplicative
forms of quantification and a PER semantics has been developed in joint
work with David Pym and Edmund Robinson.
In recent years there has been an explosion of interest in calculi for
programming with explicit memory-management operations. In particular,
there are calculi that explicitly use location and region variables as
parameters in types and terms. These calculi are often rather complex
and almost never have a denotational semantics. Together with David Pym,
I have shown how some of the essential semantic content of these calculi
(in memory models) can be captured syntactically using Bunched Polymorphism.
-
Didier Galmiche
,
LORIA, Nancy
Title BI logic, resource models and proofs
Abstract
The logic of Bunched Implications (BI) provides a logical analysis of
a basic notion of resource rich enough to provide ``pointer logic''
and ``separation logic'' semantics for programs which manipulate
mutable data structures. In order to study the provability of such
resource logics, we aim to emphasize the role of a semantic structure
called resource graph from which we can generate proofs or
countermodels. In this context, we provide a characterization of
provability in BI's Pointer Logic (PL). Then, we present a new
resource model, based on resource trees, and its related separation
logic (BI-Loc), an extension of BI with a modality for locations, for
which provability is studied.
-
Luis Caires
,
Nova, Lisboa
Title Spatial-Behavioral Types for Distributed Systems
Abstract
We discuss a type system, motivated by dynamic spatial logic, that may
be used to discipline distributed interactions in service-based systems.
Types denote spatial-behavioral properties, enabling us to formulate
semantical soundness arguments for typing and subtyping relations.
-
Silvano Dal Zilio
,
LIF, Marseille
Title Model-Checking in the Static Fragment of Ambient Logic
Abstract
We study the complexity of the quantifier-free, static fragment of ambient logic, with composition adjunct and iteration, which corresponds to a kind of regular expression language for semistructured data.
-
Damiano Mazza
,
IML, Marseille
Title Multiport Interaction Nets and Concurrency
Abstract
We consider an extension of Lafont's Interaction Nets, called Multiport Interaction Nets, and show that they are a model of concurrent computation by encoding the full pi-calculus in them. We thus obtain a faithful graphical representation of the pi-calculus in which every reduction step is decomposed in fully local graph-rewriting rules.
-
Stéphane Demri
,
LSV, Cachan
Title A temporal logic for spatial exploration
Abstract
Temporal logic is a standard formalism to express time dependencies between the states
of a given trace. This talk introduces some ideas on how could temporal logic be used to specify and verify safety properties of programs manipulating pointers.
We will present two perspectives opened by adding temporal connectives to separation logic
we are currently investigating