Subject areas:
Computer science.
Natural Sciences.
Funding type:
Stipend.
Tuition fee.
3.5 year fully-funded studentship in informatics to start in either June 2025 or October 2025.
Award details
Applications are invited for a fully-funded PhD studentship to start in June 2025 or at a later date during the 2025-26 academic year.
Project Description:
Software verification techniques have been successfully used to prove correctness of low-level programs, but verification of high-level programming languages is challenging: it requires reasoning about name binding (e.g., visible/hidden channel names, scoping rules defining local and global variable names, parameter passing and substitution of values for variables). A standard approach to deal with name binding in verification tasks is to replace names with numerical codes (de Bruijn indices). While this avoids some of the difficulties of reasoning about names in programs, conducting a formalisation in de Bruijn style is labour-intensive and imposes a significant overhead to comprehending and reusing proofs. Nominal techniques offer an alternative, user-friendly approach, which does not require to replace names with codes.
We aim to apply novel nominal techniques to simplify the handling of names and binders in programming languages and verification tasks (e.g., verification of blockchain languages, security policies, etc). For this, we aim to develop a core nominal calculus and use it as a basis to enrich with nominal features verification frameworks such as Maude and K.
Award value
The studentships are funded for 3.5 years and include Tuition Fees, a Stipend at the UK Research Council rate (plus London weighting) and an allowance for research consumables and travel.
Eligibility criteria
Award open to UK and overseas students.
Applicants should have a First-class undergraduate degree or a Distinction at MSc level in Computer Science or Mathematics. In exceptional cases other qualifications and experience may be considered and all applications will be assessed on their merit as appropriate.
Application process
Applications should be submitted by the end of December for a start in June 2025 and by the end of May for a start in October 2025. Applications will be assessed as they arrive so submit as early as possible.
To be considered for the position candidates must apply via King’s Apply online application system. Details are available here.
Applicants should email Professor Maribel Fernandez before submitting the application, and include a summary of their academic background, research interests and any relevant previous experience.
Selection process
Applicants will be shortlisted based on the documents submitted and, if selected, will be interviewed by a panel of 2-3 academics from the Department.
Contact Details
Professor Maribel Fernandez, Department of Informatics, Maribel.Fernandez@kcl.ac.uk