As of January 2008 I am an EPSRC Advanced Research Fellow, working on Semantics of nondeterminism: functions, strategies and bisimulation.
Here are my lecture notes on Typed Lambda-Calculus from Midlands Graduate School.
My research has explored call-by-push-value, an endlessly fascinating programming calculus that underlies the call-by-value and call-by-name paradigms. My book on the subject was published in 2004. Email me for more information about it.
More generally, anything related to denotational semantics, including games, categories and nondeterminism, interests me. Here are some papers.
If you are interested in doing a PhD in anything like this, then read this and email me.
room 216
telephone +44 121-414-4792
email P.B.Levy@cs.bham.ac.uk