Dear all, We invite applications for PhD study at the University of Birmingham. We are a group of theoretical computer scientists and mathematicians who explore fundamental concepts in computation and programming language semantics. Among our research interests are category theory, lambda-calculus and computational effects, topology, constructive mathematics, game semantics, and program compilation. Our group currently has 11 permanent staff and 11 PhD students. We have a weekly seminar, as well as more informal meetings and reading groups. Information on all of this can be found on our webpage: http://www.cs.bham.ac.uk/research/groupings/theory/ Information about PhD applications may be found here: http://www.cs.bham.ac.uk/admissions/postgraduate-research/ If you are considering applying, please contact any of us. We will be very happy to discuss the opportunities available. Best regards, The Birmingham CS theory group -- Benedikt Ahrens <b.ahrens@cs.bham.ac.uk> semantics of type theory, computer theorem proving, categorical structures in programming Mart??n Escard?? <m.escardo@cs.bham.ac.uk> topology, computation with infinite objects, constructive mathematics, intuitionistic type theory Dan Ghica <d.r.ghica@cs.bham.ac.uk> game semantics, heterogeneous computing, model checking Achim Jung <a.jung@cs.bham.ac.uk> mathematical structures in the foundations of computing: logic, topology, order Paul Blain Levy <p.b.levy@cs.bham.ac.uk> denotational semantics, computational effects and call-by-push-value, nondeterminism, category theory, coalgebra, game semantics Dave Parker <d.a.parker@cs.bham.ac.uk> formal verification, probabilistic model checking Uday Reddy <u.s.reddy@cs.bham.ac.uk> semantics of state, separation logic Eike Ritter <e.ritter@cs.bham.ac.uk> security protocol verification Hayo Thielecke <h.thielecke@cs.bham.ac.uk> abstract machines, concurrent and functional programming, software security Steve Vickers <s.j.vickers@cs.bham.ac.uk> constructive mathematics and topology, category theory and toposes Noam Zeilberger <n.zeilberger@cs.bham.ac.uk> categorical semantics of type systems and ??-calculus, substructural logic and proof theory, interactions with combinatorics [For admin and other information see: http://www.mta.ca/~cat-dist/ ]