SHF: Small: Relational Parametricity for Program Verification

标题：SHF：Small：用于程序验证的关系参数软件市场目前估计每年价值5000亿美元，随着软件变得越来越普遍，这个数字很可能会实际大幅增长。软件的一个重要方面是它是正确的，也就是说，软件做的是预期的事情，不会出错。即使iPod和手机等日常设备出现故障也是不方便和令人沮丧的，但软件泄露信用卡详细信息或投票记录、导致飞机坠毁、未经授权发射核武器或危及全球金融部门可能会导致前所未有的、显然不可接受的全球不确定性。程序的不断增长的规模和复杂性使得正式的验证方法-它使用数学技术来确保程序实际上执行它们设计要执行的计算，而不是执行非预期的计算-对于构建真正安全可靠的软件越来越重要。这项研究的更广泛的影响是使开发更好、更广泛适用的形式化程序验证方法成为可能，从而有助于确保即使是大型复杂软件系统也能被证明是正确的。逻辑关系是关系参数的基础，它提供了一种直接从系统本身证明软件系统属性的方法。到目前为止，已经为许多现代编程语言和验证系统的核心片段开发了逻辑关系。然而，这是通过复杂的、不可重复使用的逻辑关系的巨大星座来实现的，而不是通过从基本原则出发呼吁它们的统一构建和可转移发展。这项研究旨在通过为逻辑关系的构建提供一个公理框架来改善当前的最新水平。该框架是原则性的、概念简单、全面、统一和预测性的。这项研究的智力价值在于它阐述和使用了范畴论的基本结构，以解决在复杂环境中构建逻辑关系和概念化关系参数的重大技术问题。它还在于这项研究将导致的新的和统一的参数公式，以及这一新框架在特定的最先进的计算问题中的应用。为确保其被采纳，将为新框架提供逻辑和工具支持。虽然该工具将允许用户试验该框架，但来自他们实际经验的反馈将进一步加强参数设置的新基础。

Title: SHF: Small: Relational Parametricity for Program VerificationThe software market is currently estimated at $500 billion per year, and this figure is likely to grow significantly in real terms as software becomes ever more ubiquitous. One crucial aspect of software is that it be correct, i.e., that software does what's intended and does not go wrong. Even failures of everyday devices like iPods and mobile phones are inconvenient and frustrating, but software leaking credit card details or voting records, causing an airplane to crash, launching nuclear weapons without authorization, or compromising the global financial sector can lead to unprecedented and clearly unacceptable global uncertainties. The ever-growing size and sophistication of programs makes formal verification methods --- which use mathematical techniques to ensure that programs actually perform the computations they are designed to carry out and do not perform unintended ones --- increasingly critical for building truly secure and reliable software. The broader impact of this research is to make possible the development of better and more widely applicable formal program verification methods, and, thereby, to help ensure that even large and sophisticated software systems are provably correct.Relational parametricity is a key technique for formally verifying properties of software systems. Logical relations, upon which relational parametricity is based, provide a means of proving properties of a software system directly from the system itself. Logical relations have by now been developed for core fragments of many modern programming languages and verification systems. However, this has been accomplished by way of an enormous constellation of complicated and non-reusable logical relations, rather than by appealing to their uniform construction and transferrable development from fundamental principles. This research aims to improve the current state-of-the-art by providing an axiomatic framework for the construction of logical relations. The framework is principled, conceptually simple, comprehensive, uniform, and predictive. The intellectual merit of this research lies in its exposition and use of essential structures from category theory ("fibrations") to address the significant technical problems of constructing logical relations, and conceptualizing relational parametricity in sophisticated settings. It also lies in the novel and uniform formulation of parametricity to which this research will lead, and the application of this new framework to specific state-of-the-art computational problems. To ensure its uptake, a logic and tool support for the new framework will be provided. While the tool will permit users to experiment with the framework, the feedback from their practical experiences will further fortify the new foundations for parametricity.