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

Please email updates to*mjp41* (Last updated: Sun Dec 31 10:52:13 GMT 2006
)

**Mathematical models**(Fiore, Pitts, Winskel) for- functional computation;
- concurrent computation; and
- combinatorics and the analysis of algorithms

- 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)- Network protocol design & analysis
- Meta-routing

**Separation Logic**(Parkinson) verifying- object-oriented programs;
- concurrent programs; and
- low-level programs.

Please email updates to