Project Code: ECR_2024_10
Main Supervisor: Hadi Shafei
Co-Supervisor: Illias Tachmazidis
Project Introduction
There are numerous cases in the history of mathematics and computer science where false results were published in textbooks or peer reviewed journals and the errors remained undetected for long periods of time. This is a serious issue that exists despite the best effort of journal referees and using interactive theorem provers to formalize the proofs is the proper way to address it. An interactive theorem prover is a software that at the core is usually a functional programming language equipped with dependent types. This allows the programmer to state and prove mathematical statements of arbitrary complexity in the same environment.
Project Details
This project aims to formalize computational complexity theory, a field in theoretical computer science that investigates the inherent difficulty of solving computational problems. Proofs in computational complexity theory tend to be long and complicated which makes the proofs in this field more error prone. Despite the success of formalization projects in mathematics and computer science, formalizing computability and complexity theory has not received a similar attention.
The benefits of such a project are manifold. On one hand, errors in the existing proofs in papers and textbooks can be found and potentially fixed, which leads to a more reliable body of knowledge. It also creates a better picture of logical requirements for each theorem in the field which can lead to new ideas, perspectives, and results. Finally, formally verified body of work in this project will be a building block for formalizing new proofs in the future, like a library in a regular programming language. This is particularly important since it is believed by many that machine-checked proofs will be the norm in the near future. Formalizing computational complexity theory from the ground up is an ambitious project that requires expertise in different areas of theoretical computer science and logic. Similar projects have been started in different areas of mathematics including abstract algebra, category theory, mathematical logic, and number theory to name a few. This research will improve the reliability of the existing proofs and works as the building block for the formalized proofs in this area in the future. Formalization of the theorems and proofs is also beneficial for a better understanding of the minimal axiomatic requirements of every theorem in computational complexity theory, which results in a much clearer understanding of the field and can potentially inspire new insights.
This project addresses a gap in the field of formal verification. The little work that has been done consists of scattered results here and there and what is missing is a systemic approach to formalize the field of computational complexity theory. This project’s goal is to start this approach.
Computational complexity theory is a vast area and has numerous subfields. A successful verification of the foundations of computational complexity theory opens the door to a huge number of research projects in the future that will be based on this project’s formalization.
Some areas of computational complexity theory are the theoretical foundations for cryptography. This project, and the subsequent developments, will give us more confidence in the correctness of the theorems that cryptographic notions are built upon. Formalized results will form several libraries in the archive of the interactive theorem prover used in the project (Coq). These libraries will be used to further develop the formalization in the later projects. There is potential for several journal and conference proceedings publications.
Type of Award: Doctor of Philosophy (PhD).
Eligibility: First Class or Upper Second-Class Honours degree or equivalent in a relevant subject area, please refer to the entry requirements on the specific projects being advertised.
Location: Huddersfield.
Funding: 3 years full time research covering tuition fees and a tax-free bursary (stipend) of £5,000 per annum.
Duration: 3 years full-time plus 12 months writing up (please note that no funding is available for the writing up period).
Closing date: 5th January 2024
Start date: 15th April 2024
Application details
Complete the Expression of Interest form and include the following:
- Qualification certificates and academic transcripts
- Two-page curriculum vitae (CV)
- Passport or alternative ID
- Proof of English language requirements (if applicable)
Completed forms, including all relevant documents should be submitted via-email to sce.research.admin@hud.ac.uk.
Please note: if you do not attach all the relevant documentation prior to the closing date of 26th January 2024 your application will not be considered.