FindAPhD Weekly PhD Newsletter | JOIN NOW FindAPhD Weekly PhD Newsletter | JOIN NOW

Foundational Effectful Type Theories


   School of Computer Science

This project is no longer listed on FindAPhD.com and may not be available.

Click here to search FindAPhD.com for PhD studentship opportunities
  Dr Vincent Rahli  No more applications being accepted  Funded PhD Project (European/UK Students Only)

About the Project

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.


Funding Notes

The position offered is for three and a half years full-time study. The value of the award is stipend; £15,609 pa; tuition fee: £4,500. Awards are usually incremented on 1 October each year.
Eligibility: First or Upper Second Class Honours undergraduate degree and/or postgraduate degree with Distinction (or an international equivalent). We also consider applicants from diverse backgrounds that have provided them with equally rich relevant experience and knowledge. Full-time and part-time study modes are available.
If your first language is not English and you have not studied in an English-speaking country, you will have to provide an English language qualification.

References

http://www.cs.bham.ac.uk/~rahliv/articles/open-bar-CSL2021.pdf
http://www.cs.bham.ac.uk/~rahliv/articles/bar-induction-lics-short.pdf
http://www.cs.bham.ac.uk/~rahliv/articles/continuity-journal-mscs.pdf

How good is research at University of Birmingham in Computer Science and Informatics?


Research output data provided by the Research Excellence Framework (REF)

Click here to see the results for all UK universities
Search Suggestions
Search suggestions

Based on your current searches we recommend the following search filters.

PhD saved successfully
View saved PhDs