Language Embeddings for Proof Engineering
Lead Research Organisation:
University of Bristol
Department Name: Computer Science
Abstract
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
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
Publications
Kavvos G
(2024)
Two-Dimensional Kripke Semantics I: Presheaves
Kavvos G
(2024)
Two-dimensional Kripke Semantics II: Stability and Completeness
in Electronic Notes in Theoretical Informatics and Computer Science
| Description | This award supported the development of Two-Dimensional Kripke Semantics, which is a new way of understanding the semantics of certain types of intuitionistic and modal logics. Such logics are relevant to Computer Science, as their proofs have deep computational content: they can be used to specify the behaviour of computer systems, and to enable computer-assisted reasoning and mathematical proof - a key component of ensuring the safety of critical systems, especially in the age of AI. The techniques developed drew a very long parallel, connecting the relational semantics developed by the revolutionary work of the analytic philosopher Saul Kripke (1940 - 2022) with proof theory and the modern use of intuitionistic and modal logic in programming languages and proof assistants. This demonstrated that proofs in this logic have previously-unnoticed categorical structure, which is uniquely determined by a mathematical concept known as a Kan extension. Furthermore, this award has been used to develop a new approach to Functional Logic Programming. We developed a new approach to the semantics of Functional Logic Programs, based on the mathematics of algebraic theories. This will lead to new ways of implementing declarative languages, which can be used for programming by specifying what is to be done, rather than how it is supposed to be done. Finally, and most closely associated with the original objectives of the grant, we have recently developed a new type of Language Embedding, called a Contextual Embedding. This is a type of language embedding that is maximally flexible: while it is easy to use within a programming language and/or proof assistant, it also maintains maximal information about embedded programs, in the sense that they can be turned back into an Abstract Syntax Tree (AST) whenever required. This is poised to lead better implementations of Domain-Specific Languages, which can be used for a variety of purposes in software development and other applications. |
| Exploitation Route | The material on Two-dimensional Kripke Semantics paves the way to new developments in logic and its use for certified computer systems and software. The results on Functional Logic Programming can be used for the development of new programming languages and paradigms, leading to faster and more expressive implementations. Finally, the embedding techniques discovered can be used by developers to make their own Domain-Specific Language that is tailor-made to an individual purpose. This language can then be deployed and used by end-users who do not necessarily know how it works behind the scenes, but achieves their particular purpose. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| Description | Two-dimensional Kripke Semantics and World Models |
| Amount | £136,977 (GBP) |
| Organisation | Advanced Research and Innovation Agency (ARIA) |
| Sector | Public |
| Country | United Kingdom |
| Start | 08/2024 |
| End | 09/2025 |