SHF: SMALL: Semantically and Practically Generalizing Graded Modal Types

在过去三十年的过程中，研究编程语言的计算机科学家致力于两个主要问题：如何将软件验证合并到典型的软件开发人员的工作流程中，以及如何扩展软件验证以支持对数据使用的推理，例如，防止滥用内存和套接字句柄。这个项目的主要新颖之处在于纠正数据滥用的问题：该研究概括并结合了用于数据使用推理的程序逻辑，以及现代编程语言中使用的验证工具的功能，在单一实用的通用编程语言中。该项目的优点是：(1)发展了一种新的一般理论，其他人可以用来研究和采用这种新的组合；(2)一种新的编程语言Tenli，它包含了这种新的强大组合；(3)为本科和研究生阶段的教学资源软件验证设计新的教材。这项工作的一个主要的更广泛的影响是在这个项目中纳入了广泛的学生，例如，来自佐治亚州研究型大学奥古斯塔大学的本科生，佐治亚州历史悠久的文理女子学院卫斯理学院，佐治亚州历史悠久的私立卫理公会黑人大学克拉克亚特兰大，以及奥古斯塔大学的第一批研究生。该项目结合了两种强大的验证方法：(1)基于类型的验证，以及(2)通过分级模态类型跟踪数据使用情况。分级模态类型被推广到支持对广泛的数据使用跟踪的推理，包括对命令式数据结构的推理。基于伴随逻辑的概念，提出了一种新的梯度模态类型理论，并在此基础上开发了一种新的实用的通用依赖类型编程语言Tenli。此外，正在Tenli内部进行几个案例研究，以评估其实用性。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Over the course of the last thirty years, computer scientists studying programming languages have worked on two major problems: how to incorporate software verification into the typical software developer's work flow, and how to extend software verification to support reasoning about data usage, for example, preventing the misuse of memory and socket handles. The main novelties of this project are to rectify this problem of misuse of data: the research generalizes and combines program logics for reasoning about data-usage, and the power of verification tools used in modern programming languages, within a single practical general-purpose programming language. The project's merits are: (1) The development of a new general theory that others can use to study and adopt this new combination; (2) A new programming language, Tenli, that encompasses this new powerful combination; and (3) The design of new pedagogical materials for teaching resourceful software verification at both the undergraduate and graduate levels. A major broader impact of this work is the incorporation of a wide range of students in this project, e.g., undergraduate students from Augusta University, a research university in Georgia, Wesleyan College, a historical liberal arts women's college in Georgia, and Clark Atlanta, a private Methodist historically black university in Georgia, and the first cohort of graduate students at Augusta University.This project combines two powerful verification methodologies: (1) type-based verification, and (2) data-usage tracking through graded modal types. Graded modal types are generalized to support reasoning about a wide range of data-usage tracking including reasoning about imperative data structures. Both a new theory of graded modal types based on the notion of adjoint logics and a new practical general-purpose dependently-typed programming language, Tenli, are developed based on this new theory. Furthermore, several case studies within Tenli are being conducted to gauge its practicality.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.