Research Associate in Higher-order Constrained Horn Clauses
Job number ACAD104406
Division/School School of Computer Science, Electrical and Electronic Engineering and Engineering Maths
Contract type Open Ended
Working pattern Full time
Salary £33,797 - £38,017
Closing date for applications 17-Feb-2020
The Department of Computer Science at the University of Bristol is seeking to appoint a Research Associate to work on EPSRC-funded project “Higher-order Constrained Horn Clauses: A New Approach to Verifying Higher-order Programs”.
The successful applicant will work with Dr Steven Ramsay in a vibrant and growing Programming Languages group at the University of Bristol. The project is a larger collaboration with doctoral students and postdoctoral researchers in the group of Prof Luke Ong in the University of Oxford and outstanding international visiting researchers.
Higher-order programming (especially functional programming) holds a lot of promise for creating software that is free of bugs: programs are developed compositionally, effects are carefully managed, interfaces are explicit, and the semantic foundations are clean and beautiful. Yet techniques for formally verifying that higher-order programs are free of bugs (or otherwise identifying them) lag their counterparts in imperative programming. The successful applicant is expected to undertake research with the goal of redressing this inconsistency, by developing new theory and tooling based on higher-order logic. There are many directions, but it will be desirable to have prior experience in at least one of the following:
Type systems and lambda calculus Higher-order logic Software verification (e.g. software model checking) Compilers for functional programming languages Programming language semantics
Applicants must have obtained or be close to obtaining a PhD in Computer Science, Mathematics or a related subject. The position is offered for a fixed term of 3 years. The expected start date is 1 March 2020 or as soon as possible thereafter. Informal enquiries can be made to Dr Steven Ramsay (email@example.com).
We welcome applications from all members of our community and are particularly encouraging those from diverse groups, such as members of the LGBT+ and BAME communities, to join us.