SHF: SMALL: Practical Linear Types for Safe Protocols

软件错误经常出现，因为程序的一个组件没有正确地遵循一个定义良好的协议来访问一些有状态的资源。常见的例子包括滥用操作系统提供的资源句柄的程序，多次错误地释放相同的内存或其他资源，或者未能正确地对复杂程序模块进行顺序调用。这样的协议违反会导致软件崩溃或意外的行为，可能会带来灾难性的后果。该项目的目标是开发编程语言技术，以允许软件开发人员方便地描述协议overstateful资源。这项技术将在设计时通过静态检查程序是否正确地遵循了所需的协议来发现这些错误，从而排除了广泛的软件缺陷。 新的语言机制将是通用的，实用的，适用于从内存管理到传统协议实现的各种应用。研究人员将创建一个编译器基础设施原型，并通过机器检查类型可靠性证明来建立方法的正确性。 该项目的主要广泛影响是开发技术，以帮助在软件设计生命周期中尽早消除此类编程错误，从而降低构建正确可靠软件的成本。

Software errors frequently arise because a component of the program doesnot correctly follow a well-defined protocol for accessing some statefulresource. Common examples include programs that misuse resource handlesprovided by the operating system, incorrectly deallocate the same memoryor other resource multiple times, or fail to properly sequence calls toa complex program module. Such protocol violations lead to softwarecrashes or unintended behavior, potentially with disastrousconsequences.The project objective is to develop programming language technology toallows software developers to conveniently describe protocols overstateful resources. This technology will uncover such bugs at designtime by statically checking whether the program is appropriatelyfollowing the desired protocols, thereby ruling out the wide class ofsoftware flaws. The new language mechanisms will be general purpose,practical, and suitable for use in a wide variety of applicationsranging from memory management to traditional protocol implementation.The researchers will create a compiler infrastructure prototype andestablish the correctness of the approach by a machine-checked proof oftype soundness. The primary broader impact of the project is thedevelopment of technology to help eliminate such programming errorsearly in the software-design life cycle to decrease the cost of buildingcorrect, reliable software.