Abstract

I will be talking about joint work with Peter Sewell on syntax-free models of name-passing processes. I will begin by reviewing some of the reasons which have led Peter and me 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.