[TYPES] postdoc position: semantics of nondeterminism

[Paul B Levy]

Dear colleagues,

A postdoctoral Research Fellowship lasting 32 months is available in the
School of Computer Science, University of Birmingham, starting any time
from 1 July 2005 to 1 January 2006, working in the semantics of
nondeterminism.  The application deadline is 22 July 2005.  Application
details can be found at

http://www.punit.bham.ac.uk/vacancies/furtherParticulars.htm?refNo=36914

The School of Computer Science is a major centre for research and teaching
in Computer Science and has around 130 researchers, with a lively and
friendly atmosphere that encourages research straddling different themes.  
The vibrant Theory Group spans the spectrum from programming languages to
mathematical foundations. Its research includes game, domain, effect,
pointer and categorical semantics, topology, logic, model-checking and
much else besides. The School has recently hosted the Midlands Graduate
School (April 2005) and Mathematical Foundations in Programming Semantics
(May 2005).

Semantics of nondeterminism
---------------------------

To reason about a computer system, it is often necessary to idealize it as 
nondeterministic, i.e. possessing a range of possible behaviours. The 
factors that determine its actual behaviour are too low-level and complex 
to consider explicitly. But this apparently simple idea has ramifications 
for the theory of programming language semantics that are not well 
understood. They centre on the question: what does it mean for 2 programs 
to be equivalent? Previous research has used mathematical structures known 
from the theory of deterministic programs. But these have limited 
applicability to nondeterministic programs, and lead to somewhat awkward 
notions of equivalence. This research will proceed in the opposite 
direction: begin with certain computationally natural notions of 
equivalence, and investigate what structures they lead to.

Aspects of this research may include:

- formulating game semantics that build on existing game models and on 
existing ways of reasoning about nondeterminism (e.g. Howe's method for 
congruence of bisimilarity)

- studying higher-order languages with nondeterminism, building on
existing calculi (e.g. call-by-push-value, Affine HOPLA, etc.), and
diverse semantics of such languages

- analyzing definability of functions at low order.

There is plenty of scope for developing these themes in different
directions.

Applicants must hold a PhD (or expect to attain one before taking up the 
appointment). A research background in any or all of the following would 
be useful:

    * category theory
    * semantics of programming languages
    * game semantics
    * semantics of concurrency

Please do not hesitate to contact me with any queries.

Regards
Paul

-- 
Paul Blain Levy              email: pbl at cs.bham.ac.uk
School of Computer Science, University of Birmingham
Birmingham B15 2TT, U.K.      tel: +44 121-414-4792
http://www.cs.bham.ac.uk/~pbl