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.
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.
this project we aim to:
- Generalize some of the
existing results from the meta-theory of SOS in order to improve their
- Establish new meta-results regarding
- Provide compositional reasoning
methods for logics of security;
- Apply the resulting theory to a
number of case-studies dealing with modern programming languages 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