PROJECT OVERVIEW

The development of a formal semantics for programming and specification languages is a necessary first step towards rigorous reasoning about them. For instance, a formal semantics allows one to prove the correctness of language implementations, and is a prerequisite for proving the validity of program optimizations.

Operational semantics is a widely-used methodology to define formal semantics for computer languages, which represents the execution of programs as step-by-step development of an abstract machine. Structural Operational Semantics (SOS) was introduced by Gordon Plotkin as a logical and structural approach to defining operational semantics. The logical structure of SOS specifications supports a variety of reasoning principles that can be used to prove properties of programs whose semantics is given using SOS. Moreover, SOS language specifications can be used for rapid prototyping of language designs and to provide experimental implementations of computer languages. Thanks to its intuitive appeal and flexibility, SOS has become the de facto standard for defining operational semantics, and a wealth of programming and executable specification languages have been given formal semantics using it.

In recent years much work on the underlying theory as well as on the practice of SOS has been carried out---see, e.g., the papers in this bibliography maintained by MohammadReza Mousavi. However, a substantial amount of work remains to be done in this rapidly-evolving area of research.

• Extant classic results in the theory of SOS seem to be amenable to further generalizations. These generalizations would not only be of theoretical interest, but would also increase the scope and the applicability of the theory.
• Several new semantic issues have become prominent in recent years. Notions related to security such as non-interference, authentication, availability and anonymity are typical examples of issues that have yet to be addressed satisfactorily by the SOS meta-theory. Furthermore, compositional reasoning techniques for logics of security are very much sought by researchers in the field, and seem to be both useful and feasible in light of recent developments in the fields of security and SOS.

In this project we aim to:

• Generalize some of the existing results from the meta-theory of SOS in order to improve their applicability;
• Establish new meta-results regarding security-related notions;
• Provide compositional reasoning methods for logics of security;
• Apply the resulting theory to a number of case-studies dealing with modern programming languages and formalisms; and
• Develop prototype tool support for experimenting with SOS language specifications.

This project will bring disparate results (old and new) under one roof, and will open up the possibility of more easily exploring their interactions, more easily generalizing them, and more easily implementing them.