Mathematical Models for Concurrent and Mobile Computation

Project Details

Description

The overall aim of this research was to develop and refine mathematical models for interacting programs, and in particular for features that arise from naming, location, and mobility of both data and computation.

Mathematical models help us to understand the behaviour of complex systems: by providing a language to describe such systems, and potentially tools to analyse and predict that behaviour.

In this project the complexity arises from trying to reason about programs that connect with each other in order to communicate; that change those connections; and that move from one computer to another.

The specific objectives of the project deal with three linked areas: the pi-calculus, an established system for describing concurrent computation; names and the binding of names to values; and use of machine-checked proofs as guarantees of program behaviour.

This last area, "proof-carrying code", has a direct practical use in providing security certificates for Java applications and other app frameworks. Proof-carrying code complements existing digital signatures with "digital evidence": while signatures tell us who supplied a program, mathematical proofs can guarantee the behaviour of the code itself.

Layman's description

The overall aim of this research is to develop and refine mathematical models for interacting programs, and in particular for features that arise from naming, location, and mobility of both data and computation.
Mathematical models help us to understand the behaviour of complex systems: by providing a language to describe such systems, and potentially tools to analyse and predict that behaviour.

Key findings

The project made significant specific advances in mathematical modelling of different kinds of computation.  Some of these involved new collaborations with researchers in Edinburgh and beyond:



1. Free-algebra models for the pi-calculus, the first application of Plotkin-Power equational theories to concurrent systems.  These give a modular and systematic description of a family of fully-abstract models for communicating mobile processes.



2. A type theory for formal reasoning about names and binding, introducing fresh dependent products, sums and the novel "freefrom" type constructor.  (Collaboration with Schoepp, Edinburgh.)



3. The invention of "nominal games" and the first fully-abstract model for dynamic name creation in sequential programming languages.  (Collaboration with Ong et al., Oxford.)



4. The technique of "TT-lifting" for transforming concrete properties of data into observable properties of computation, for arbitrary notions of computation. (Collaboration with Lindley, Edinburgh.)



5. The Mobile Resource Guarantee framework for proof-carrying code: a resource-aware compiler, bytecode logic, and proof-checking client.  (Collaboration with MRG group in Munich and Edinburgh.)
StatusFinished
Effective start/end date1/07/0230/06/07

Funding

  • EPSRC: £246,763.00