Mathematical Structural Operational Semantics
Lead Research Organisation:
University of Edinburgh
Department Name: Sch of Informatics
Abstract
Structural operational semantics (SOS) is a formal method of describing the meaning and behaviour of programming languages. Such methods are needed for automated program analysis, verification, translation or even construction.An SOS specification describes how programs can perform actions and, at the same time, transform to other programs. The actions that a program may take are determined by the actions of its subprograms. This semantical method is popular among researchers, and many simple languages have been specified this way, but a comprehensive theory is needed to help language designers write well-structured and well-behaved operational semantics.We aim at such a formal, mathematical theory of SOS. We plan to treat formats for operational specifications that guarantee some desirable properties of programs, provide logics for reasoning about programs, enable reasoning about translations between programming languages, and give means for the modular construction of operational semantics.Such a theory will benefit programming language designers, facilitating the creation of new languages, the modification of existing ones, and the analysis of programs.
Organisations
People |
ORCID iD |
Gordon Plotkin (Principal Investigator) |
Publications
Klin B
(2007)
Bialgebraic Methods in Structural Operational Semantics
in Electronic Notes in Theoretical Computer Science
Klin B
(2007)
Coalgebraic Modal Logic Beyond Sets
in Electronic Notes in Theoretical Computer Science
Klin B
(2009)
Bialgebraic methods and modal logic in structural operational semantics
in Information and Computation
N/a Klin
(2008)
Structural operational semantics for stochastic systems