EPSRC logo

Details of Grant 

EPSRC Reference: EP/Y000242/1
Title: Language Embeddings for Proof Engineering
Principal Investigator: Kavvos, Dr A
Other Investigators:
Researcher Co-Investigators:
Project Partners:
University of Maryland
Department: Computer Science
Organisation: University of Bristol
Scheme: Standard Research - NR1
Starts: 01 December 2023 Ends: 30 November 2025 Value (£): 97,448
EPSRC Research Topic Classifications:
Computer Sys. & Architecture
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
17 May 2023 ECR International Collaboration Grants Panel 1 Announced
Summary on Grant Application Form
There are certain kinds of computer systems and devices from which we demand impeccable performance: medical devices; air traffic control systems; railway signalling; self-driving cars. In such mission-critical systems anything less than perfect performance could amount to unimaginable losses.

One way to certify a mission-critical system's behaviour is to produce a mathematical proof that it will function as expected. However, this approach merely replaces one problem with another: how can we then be sure that the proof is correct, especially when it may run to hundreds of pages of detailed technical arguments?

To solve this problem we have developed proof assistants. These are remarkable pieces of software: not only can they help us build large proofs, but they can also check the correctness of a proof on our behalf. Thus, as long as we trust the kernel of the proof assistant, we have some assurance that our proof is correct (and hence that our system/hardware/software is bug-free).

However, this solution is not perfect. Developing proofs is a challenging task, perhaps an order of magnitude more difficult than software development. This has led in the last 10 years to the creation of proof engineering, a new field of Computer Science which is concerned with the development of large mathematical proofs.

In this project we aim to make foundational contributions to one popular aspect of proof engineering, namely the formulation of Domain Specific Languages (DSLs). We aim to show that practical DSLs developed and used by proof engineers can be given a solid footing using a field of mathematical logic known as type theory.

Our results will lead to better, simpler, reusable, and more transparent ways to design DSLs. This will offer substantial benefits to proof engineers, who will then be able to employ our techniques in order to verify the safety of even larger mission-critical systems in a systematic fashion, and with less effort.

The project will be carried out by combining the theoretical background of the PI in the semantics of type theory with the practical expertise of the international collaborator, who has previously crafted development tools for testing within a popular proof assistant, Coq
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.bris.ac.uk