The work of the Theory and Semantics Group is centred round mathematical models
of a variety of languages and logics. These models are intended to be
used as a tool
for clarifying programming concepts, as a basis for specification and
verification, and
for analysing the complexity of computations. We use techniques such
as structural
operational semantics, domain theory, category theory, finite model
theory and linear
logic. Work is in progress on the underlying mathematical structures
of these, and on
their application to the study of higher order typed programming
languages, to object-based
languages, to foundational languages for concurrent, distributed and mobile
computation, to hardware description languages, and to security
problems. We work
in close collaboration with the
Automated Reasoning
Group,
Programming Research and
Systems Research Groups.
Research Themes
- Mathematical models (Fiore, Pitts, Winskel) for
- functional computation;
- concurrent computation; and
- combinatorics and the analysis of algorithms
based on
- category theory; and
- domain theory.
- Foundations of distributed computation, (Sewell, Winskel) including
- the design, semantics and implementation of distributed programming languages;
- behavioural modelling for network protocols; and
- security issues
- Finite model theory (Dawar) and its connection to
- the study of computational complexity;
- the theory of databases;
- the complexity of games; and
- the expressive power of logical formalisms
- Mechanized meta-theory(Pitts, Sewell)
- Machine-assisted support for operational semantics of programming languages
- Nominal sets (Pitts)
- Applications of nominal sets to metaprogramming languages
- Network Semantics(Griffin, Sewell)
- Separation Logic (Parkinson) verifying
- object-oriented programs;
- concurrent programs; and
- low-level programs.
Related research themes can also be found on the
CPRG and
ARG research pages.
Please email updates to mjp41 (Last updated: Sun Dec 31 10:52:13 GMT 2006
)
