Detail

Spatial-Behavioral Types for Distributed and Concurrent Programming

We discuss a type system, motivated by dynamic spatial logic, that may be used to discipline distributed interactions in concurrent, distributed and service-based systems.

Technically, in our system types denote spatial-behavioral properties definable in spatial logic, enabling us to formulate semantical soundness arguments (cf. logical relations) for the typing and subtyping relations.

However, in this talk we will focus on the key ideas of our
approach, through the presentation of a series of motivating examples, covering the technical contributions just at the intuitive level, and motivating our approach with a Java-like programming language.