SHF: SMALL: Semantically and Practically Generalizing Graded Modal Types

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

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.