A Model for Declarative Programming and

Specification with Concurrency and Mobility

June, 1999

Luis Caires

In this dissertation, we propose a framework for declarative specification and programming of modular systems with concurrency and mobility. The main contributions are the introduction and study of the core programming language Lpi, and of the dol specification logic for mobile processes. Lpi is a language that demonstrates a minimalist approach to the unification of multiple programming paradigms, by building on an interpretation of concurrent computation as proof-search in linear logic. We assess the expressiveness of Lpi as a programming language by showing that many concurrent and executable logic idioms can be reconstructed as its fragments, and also how it can motivate novel combinations of concurrent, functional, logic and object-oriented paradigms in a natural way.

Towards a more encompassing application of the Lpi model, we propose and study dol, a logic specially aimed at the specification and reasoning about structure and behaviour of concurrent mobile systems. dol integrates a mu-calculus with structural connectives that express distribution of components and privacy of names in the context of a first-order logic where quantification is performed over a structured expanding universe. This logic aims at providing a basis for the axiomatic specification of generic mobile processes at a useful level of abstraction. A bridge between the specification logic and the Lpi model is exemplified by the definition of an idiom of dol which constitutes a class-based object-oriented specification logic. We then show how a fragment of this specification logic can be compiled into Lpi, in a way such that encodings are models of specifications.

Full text

Sample chapter, about an earlier spatial logic