EPSRC Reference: 
EP/E042414/1 
Title: 
Mathematical Operational Semantics for DataPassing Processes 
Principal Investigator: 
Staton, Dr S 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Laboratory 
Organisation: 
University of Cambridge 
Scheme: 
Postdoc Research Fellowship 
Starts: 
01 June 2007 
Ends: 
31 May 2010 
Value (£): 
209,202

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
13 Feb 2007

Postdoc Fellowships Sift Panel  Computer Science

InvitedForInterview


Summary on Grant Application Form 
Operational semantics is concerned with ascribing meaning to computer programs by formally describing their evolution. A formal description of a programming language is crucial if one is to prove properties of programs. One may wish to prove that a program meets a specification: for instance, that it has no security flaws; that it interacts correctly with other systems; or that the values it computes are correct. When one specifies an operational semantics for a programming language, it is usually necessary to prove some basic properties in order to ensure the validity of reasoning techniques. These properties have to be established for every new language that is considered, and whenever an existing language is changed.We use the term 'Mathematical Operational Semantics' (MOS) to describe the process of understanding techniques from operational semantics at an abstract level. A primary motivation for this line of research is that procedures from operational semantics, at times lengthy and ad hoc, can be understood from a basic structuralist viewpoint. A second, more pragmatic motivation is that theorems that are established at this abstract level have the chance of wider application in quite general contexts. With this second motivation in mind, it is helpful to see work in MOS as occuring at three levels. The highest, most abstract and general level, is concerned with theorems of category theory, which is a powerful framework for studying mathematical concepts and structures in an abstract and general way. The intermediate level involves devising categorytheoretic models for particular kinds of system. The lowest level is the level at which most operational semanticists work, and involves particular logical frameworks for reasoning about particular systems.My proposal is to make progress at all three of these levels. I will take, as a case study, the datapassing process calculi. These calculi are basic programming languages for systems that involve concurrency and communication of structured data. For instance, if one allows the names of communication channels to themselves be communicated, then a kind of mobility arises. Another kind of structured data involves encryption; process calculi involving this kind of data have been used to model security aspects of systems.At the lowest, concrete level, the proposed work involves deriving new theorems about datapassing systems from the general results. To do this it will be necessary to investigate logical frameworks that are suitable for reasoning about datapassing systems. Frameworks of this sort are of interest to researchers in other fields, such as those interested in the formalisation of large scale programming systems. Theorems that will be extracted will be of the form: if a datapassing system is specified in a certain way, then certain properties will hold . The results will hold for datapassing systems in general. They will be tested against various semantics that have been proposed in the literature.Research at the intermediate level will involve categorytheoretic models of datapassing. I will investigate the extent to which existing models and results can be considered in the categorytheoretic domain. In this way the field of datapassing will be given a more unified theory.At the highest level of abstraction, my proposed work will involve devising abstract forms of some complex proof principles. I will focus on two topics: firstly, techniques for higherorder systems  these are systems that can receive programs as data; secondly, I will investigate ways of combining proof techniques. This research will give rise to a better, more principled understanding of the processes involved in these proof methods, and will give rise to new, concrete techniques of immediate relevance to the operational semantics community.

Key Findings 
The research results are of two kinds. First, the kind that I hoped for in achieving the objectives that I set out in my research proposal. We now have a good mathematical understanding of the semantics of datapassing process languages. (See e.g. my journal publication in Information and Computation; my LICS'08 paper; and my CALCO'09 paper.)
Secondly, the research led to important new techniques in two different areas: the semantics of local state (programs that allocate memory), and models of true concurrency. (See e.g. my MFPS'09 and FOSSACS 2010 papers on state, and my LICS'10 paper on event structures.) I am currently collaborating with researchers around Europe on these matters.

Potential use in nonacademic contexts 
This is foundational research. I anticipate potential impact on programming language design and compiler optimizations. I am currently investigating this.

Impacts 
No information has been submitted for this grant.

Sectors submitted by the Researcher 
Information & Communication Technologies

Project URL: 
http://www.cl.cam.ac.uk/~ss368 
Further Information: 

Organisation Website: 
http://www.cam.ac.uk 