EPSRC Reference: 
EP/Y000242/1 
Title: 
Language Embeddings for Proof Engineering 
Principal Investigator: 
Kavvos, Dr A 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Science 
Organisation: 
University of Bristol 
Scheme: 
Standard Research  NR1 
Starts: 
18 December 2023 
Ends: 
17 December 2025 
Value (£): 
97,448

EPSRC Research Topic Classifications: 
Computer Sys. & Architecture 


EPSRC Industrial Sector Classifications: 

Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
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; selfdriving cars. In such missioncritical systems anything less than perfect performance could amount to unimaginable losses.
One way to certify a missioncritical 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 bugfree).
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 missioncritical 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 nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

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 