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 picalculus or mobile ambients, a process configuration is described as a collection of agents that can interact via appropriate mechanisms (named channels, locations, interaction capabilities). Structuresensitive relations between processes have been proposed to reason about mobility and locality properties of a system. Among these, the socalled 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 cutelimination 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 processalgebra 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 picalculus,
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 nondivergence and
deadlockfreeness. 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 picalculus, ambient calculus and petrinets. 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 secondorder.
A secondorder 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 memorymanagement 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 (BILoc), an extension of BI with a modality for locations, for
which provability is studied.

Luis Caires
,
Nova, Lisboa
Title SpatialBehavioral Types for Distributed Systems
Abstract
We discuss a type system, motivated by dynamic spatial logic, that may
be used to discipline distributed interactions in servicebased systems.
Types denote spatialbehavioral properties, enabling us to formulate
semantical soundness arguments for typing and subtyping relations.

Silvano Dal Zilio
,
LIF, Marseille
Title ModelChecking in the Static Fragment of Ambient Logic
Abstract
We study the complexity of the quantifierfree, 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 picalculus in them. We thus obtain a faithful graphical representation of the picalculus in which every reduction step is decomposed in fully local graphrewriting 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