The University of Bath is inviting applications for the following PhD project supervised by Prof Guy McCusker in the Department of Computer Science.
Imperative programming offers fast programs and fine control over execution, but is hard to verify, mainly due to the difficulty of giving a good semantics. In this project you would investigate a new approach based on intersection types, expressed in open deduction.
Intersection types can be seen from a programming-language perspective as a type system, providing static information about program behaviour, and from a semantic perspective as a presentation of a relation-based mathematical model of programs and proofs. The novelty of this project is to use non-commutative types to model sequential computation. Expressing such types effectively is made possible by the open-deduction formalism, an approach to proof theory that can alternatively be viewed as a presentation of category-theory-based semantics. The project builds on our recent work exploring intersection types in this proof formalism. A background that includes lambda-calculus or category theory would help you make a good start on it.
Candidate requirements:
Applicants should hold, or expect to receive, a First Class or good Upper Second Class Honours degree in Mathematics or Computer Science (or the equivalent). A master’s level qualification would also be advantageous.
Non-UK applicants will also be required to have met the English language entry requirements of the University of Bath.
Enquiries and applications:
Informal enquiries are welcomed and should be directed to Prof Guy McCusker on email address [Email Address Removed].
Formal applications should be made via the University of Bath’s online application form for a PhD in Computer Science (full-time).
More information about applying for a PhD at Bath may be found on our website.
Anticipated start date: 4 October 2021.
Continue with Facebook
