The School of Computer Science at the University of Birmingham, UK, is continuously looking for strong PhD candidates. One particular field of interest is constructive type theory, where proofs can be seen as programs. Several constructive type theory-based proof assistants have been developed over the years.
However, these tools provide only limited support when it comes to effectful computations, i.e. computations that have side-effects, such as stateful, distributed, or non-deterministic computations. These forms of computation are pervasive in modern systems, where, for example, programs commonly interact with one another in a distributed manner.
We are therefore looking for a student who would be broadly interested in studying the foundations and applications of constructive logics, such as intuitionistic logic, with the aim of providing methods and tools to implement and reason about effectful computations, and studying the effect of such computations on the logical systems they are integrated in.
Topics of particular interest are, for example:
• Formally develop intuitionistic theories of effectful computations
• Develop models of intuitionistic theories of effectful computations
• Formally develop a type theory that allows reasoning about cyber-physical systems
Excellent problem solving skills and programming skills are required. In addition, the candidate must have a strong background in one of the following areas:
• Type theory
• Constructive logic
• Formal methods
• Programming languages
We want our PhD student cohorts to reflect our diverse society. UoB is therefore committed to widening the diversity of our PhD student cohorts. UoB studentships are open to all and we particularly welcome applications from under-represented groups, including, but not limited to BAME, disabled and neuro-diverse candidates. We also welcome applications for part-time study.