ISLC
Organization
Presentation
Sessions
Programme
Speakers
Participants

Interaction and Space, Logics and Concurrency

Marseille - Luminy
February 27 - March 3, 2006

Organization

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.

Thematic presentation

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.

Overview of sessions

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

Preliminary programme

Mon 27
9h-10h30 Giovanni Conforti BiLog: A Spatial Logic framework
10h30 - 11h Coffee break
11h - 12h- 30 Damiano Mazza Multiport Interaction Net and Concurrency
Tu 28
14h-15h30 Matthew Collinson Bunched and Multiplicative Polymorphism, Regions and Locations
15h30 - 16h Coffee break
16h - 17h30 Didier Galmiche BI logic, resource models and proofs
Thu 2
9h - 10h30 Luis Caires Spatial-Behavioral Types for Distributed Systems
10h30 - 11h Coffee break
11h - 12h30 Silvano Dal Zilio Model-checking in the Static fragment of Ambient Logic
12h30 - 14h Lunch
14h - 15h30 Emmanuel Beffara Concurrent realisability
15h30 - 16h Coffee break
16h - 17h30 Rémi Brochenin (remplace Stéphane Demri) A temporal logic for spatial exploration

Speakers