The Structure of Programming Languages: Syntax and Semantics

Funding Body: EPSRC

The Edinburgh Team

Prof Gordon Plotkin
Dr Daniele Turi



The main goal of the proposed research is to achieve an effective theory of programming languages, particularly, their syntax and semantics: both operational and denotational. A subsidiary goal is the understanding of logical formalisms for program specification, correctness and development. The proposed research is: foundational, aiming at a mathematical framework for formal methods and, more generally, applied formalisms in software engineering; both general and particular, ranging from general accounts of syntax and semantics to investigations of individual programming phenomena; and, to achieve effectiveness, strongly oriented to formalisms. To obtain an effective theory, we concentrate on core issues. Existing theories of abstract syntax are inadequate; we will develop improved algebraic theories, covering variable binding and structured types. For operational semantics we seek a general theory not tied to syntactic presentation, using co-algebras and distributive laws. Combining these yields a useful global bialgebraic view of programming languages. Computational effects underlie semantics. Here Moggi's monadic approach needs strengthening in several aspects, e.g., operational semantics and modularity. Linear type theories, arising from axiomatic domain theory, may yield a further improvement, incorporating an integrated treatment of parameter-calling mechanisms. There will also be some work on generic logic, computational logics, and combined formalisms for program development.