Language Embeddings for Proof Engineering

用于证明工程的语言嵌入

• 批准号: EP/Y000242/1
• 负责人: Alex Kavvos
• 金额: $ 12.42万
• 依托单位: University of Bristol
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2023
• 资助国家: 英国
• 起止时间: 2023 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FY000242%2F1
• 关键词: Language; Embeddings; Proof; Engineering

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

我们对某些类型的计算机系统和设备的性能要求无可挑剔：医疗设备；空中交通管制系统；铁路信号;自动驾驶汽车。在这样的关键任务系统中，任何不完美的性能都可能导致难以想象的损失。证明关键任务系统的行为的一种方法是产生一个数学证明，证明它将按预期运行。然而，这种方法只是用另一个问题代替了一个问题：我们怎么能确定证明是正确的，特别是当它可能长达数百页的详细技术论证时？为了解决这个问题，我们开发了证明助手。这些都是了不起的软件：它们不仅可以帮助我们构建大型证明，还可以代表我们检查证明的正确性。因此，只要我们信任证明助手的内核，我们就可以保证我们的证明是正确的（因此我们的系统/硬件/软件是无bug的）。然而，这个解决方案并不完美。开发证明是一项具有挑战性的任务，可能比软件开发困难一个数量级。在过去的十年里，这导致了证明工程的诞生，这是计算机科学的一个新领域，它与大型数学证明的发展有关。在这个项目中，我们的目标是为证明工程的一个流行方面做出基础贡献，即领域特定语言（dsl）的制定。我们的目标是证明工程师开发和使用的实用dsl可以使用称为类型论的数学逻辑领域来提供坚实的基础。我们的研究结果将带来更好、更简单、可重用和更透明的dsl设计方法。这将为验证工程师提供实质性的好处，他们将能够使用我们的技术，以系统的方式验证更大的关键任务系统的安全性，并且付出更少的努力。该项目将通过将PI在类型理论语义方面的理论背景与国际合作者的实际专业知识相结合来实施，该合作者以前曾在流行的证明助手Coq中制作开发工具进行测试