SHF: Small: Relational Parametricity for Program Verification

软件市场目前估计为每年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.