Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Peter Sewell
We are looking for PhD students
to work on the semantics of concurrent programs, focussed especially
on the relaxed memory models of real-world multiprocessors and
programming languages, funded by EPSRC
grant EP/H005633 Semantic Foundations for Real-World Systems.
This provides maintenance and fees for Home or EU students.
Applications should be received as soon as possible.
Overseas
(non-EU) students may wish to apply to the Gates/CISS/Cambridge Trusts
for the additional costs of overseas fees, for which there are annual
deadlines.
Formal applications should be
made via the usual method through the
Board
of Graduate Studies (local MPhil
students should use the `continuation' form), but please contact me
first if you are interested.
My research aims to put the engineering of real-world computer
systems on solid foundations, developing techniques -both
mathematically rigorous and pragmatically useful-
to enable the
construction of systems that are better-understood, more robust, and
more secure.
To do this requires tightly integrated theoretical and practical
research, spanning a range of Computer Science.
This is, broadly, applied semantics: I work in
programming languages, networking, and security,
developing and using techniques from
semantics, type systems, automated reasoning, and concurrency theory.
Relaxed memory models must be
rigorous. In EC^2.
Francesco Zappa Nardelli, Peter Sewell, Jaroslav Sevcik, Susmit
Sarkar, Scott Owens, Luc Maranget, Mark Batty, and Jade Alglave
The Semantics of Power and ARM Multiprocessor
Machine Code
(in DAMP
2009).
Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit
Sarkar, Peter Sewell, and Francesco Zappa Nardelli. Note that the
model presented here has some major flaws; further work is in
progress.