# The Structure of Programming Languages: Syntax and
Semantics

## Funding Body: EPSRC

- Grant value 530,309 pounds

## The Edinburgh Team

- GRANT HOLDERS:
- Prof Gordon Plotkin
- OTHER PARTICIPANTS:
- Dr Daniele Turi

## Objectives

- To find a theory of abstract syntax widely applicable to
programming languages, especially for variable binding and
structured types.
- To find a flexible presentation-free account of operational
semantics applicable to a wide variety of computational effects and
abstract syntax.
- To establish core formalisms for computational effects,
particularly extensions of the computational lambda calculus and
type theory for linear logic.
- To bring axiomatic domain theory to some state of
maturity.
- To make a solid start on a closely correlated program of
generic and particular research in logics of computation.

## Summary

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.