[TYPES] PhD studentship

[Hayo Thielecke]

=========================================================================

School of Computer Science, University of Birmingham
Ph.D. Studentship in separation logic and intermediate languages

=========================================================================

One PhD studentship is available in the School of Computer Science at the
University of Birmingham for research on reasoning about intermediate and
assembly languages in the compilation of high-level languages, using
continuations and separation logic.

Transformation into Continuation Passing Style (CPS) makes all control
transfers explicit, so that procedure call is broken down into two jumps,
just as in assembly language. However, since CPS is usually based on the
lambda calculus, it does not make storage explicit (such as the format of
activation records). Separation Logic has been developed over the last few
years to reason about pointers and storage. The aim of this research is to
add Separation Logic to CPS. Thus it will be possible to move closer to a
realistic implementation than would be possible using other approaches,
such as abstract machines, which still have very idealized views of
run-time data structures.

The studentship is available for UK and European applicants who want to
work full time on their research degree and lasts for up to three years.
Candidates should have, or be predicted to gain, a very good degree in
computer science, mathematics or a relevant scientific discipline.
Informal inquiries are welcome; please mail H.Thielecke at cs.bham.ac.uk.

Information about admission for PhD in Computer Science at the University
of Birmingham is available at

http://www.cs.bham.ac.uk/study/postgraduate-research/.

Applications can be made until 15th July 2005.