Peter D Mosses
Many of the topics mentioned below are involved in PLanCompS (Programming Language Components and Specifications), a 4-year joint research project based at Swansea, RHUL and City, funded by EPSRC, with project partner Microsoft Research Cambridge, 2011–2015.
Semantics of Programming Languages
A formal semantics of a programming language deﬁnes the computational behaviour of all programs in the language, just as a formal grammar deﬁnes their syntax.
The main aim of my research in the area of semantics is practical applicability, and I have focussed on improving the modularity of semantic specifications. My most recent work on component-based semantics proposes an incremental approach to the development of semantic specifications, with a high degree of reusability. I'm also developing a component-based approach to proving algebraic properties of programming constructs.
A further aim is to provide an online repository of reusable independent specifications of basic programming constructs. I also intend to develop a digital library of formal specifications of programming languages.
I've written several introductions to formal semantics, generally focussing on pragmatic aspects – in particular, on modularity.
This is a general framework for reusable semantic descriptions of individual programming constructs, developed since 2001 – initially for action semantics with Kyung-Goo Doh (Hanyang, Korea). Its practicality and scalability will be tested in the PLanCompS project, by giving component-based specifications of major languages such as C# and Java.
Modular SOS (MSOS and I-MSOS):
MSOS is modular variant of Gordon Plotkin's Structural Operational Semantics, developed since the late 1990s. It allows the semantics of individual programming constructs to be specified independently, which is of crucial importance for the PLanCompS project.
Action Semantics is a modular hybrid of denotational and operational semantics, developed since 1985, together with David Watt (Glasgow).
A variant of Action Semantics has been exploited by the Object Management Group in connection with the Model Driven Architecture (MDA) technology and the Uniﬁed Modelling Language (UML).
Abstract Semantic Algebras:
This modular hybrid of denotational and algebraic semantics was explored in the early 1980s.
As a graduate student at the Programming Research Group in Oxford in the early 1970s, I worked on the framework developed by Dana Scott and Christopher Strachey.
Tools are needed to support the development, validation, and use of semantic descriptions. I have implemented tools for denotational semantics, action semantics, MSOS, and constructive semantics.
This prototype tool provides support for constructive action semantics. It is based on The Meta-Environment, developed with Mark van den Brand (then at CWI, Amsterdam) and Jørgen Iversen (then at Aarhus) 2001-2005. It has not been released, as it requires updating to work with the current version of the Meta-Environment.
Prolog MSOS Tool:
I have implemented a tool in Prolog to support the teaching of formal semantics using Modular SOS. A new version of the tool is being used in the PLanCompS project.
MAT was a prototype tool for action semantics and MSOS, based on Maude, developed with Christiano Braga and Hermann Hauesler (then at PUC, Rio de Janeiro, Brazil) and José Meseguer (then at SRI International, USA), 1998–2001. It has been superseded by MMT, the Maude MSOS Tool.
The ASD Tools supported the original version of action semantics. They were based on the ASF+SDF Meta-Environment, and developed with Arie van Deursen (then at CWI, Amsterdam) in the mid-1990s.
SIS was the ﬁrst semantics implementation system for running programs according to their denotational semantics, developed 1975–79. It was written in BCPL, and ported to several operating systems.
Algebraic Speciﬁcation Frameworks
This area concerns the formal speciﬁcation of requirements and design for software. My contributions here have focussed mainly on frameworks that support algebraic (axiomatic) speciﬁcations of data, functions, and processes.
CASL, The Common Algebraic Speciﬁcation Language, was developed by CoFI (the Common Framework Initiative for algebraic speciﬁcation and development of software). I was the overall coordinator of CoFI 1995-98, coauthor of the CASL User Manual with Michel Bidoit, and editor of the CASL Reference Manual.
Algebraic Higher-Order Set Theory:
This framework involves a restriction of Z to Horn-clause logic and non-extensional models. It was developed with Claus Hintermeier and Hélène Kirchner (Nancy, France) 1995–99.
This is a variety of Horn-clause logic that allows algebraic speciﬁcation of type constructors. It was developed in the late 1980s, and used as the meta-notation for action semantics until the end of the 1990s.