SHF:Small:RUI: Semantic Complexity of Advanced Data Types

SHF:Small:RUI：高级数据类型的语义复杂性

• 批准号: 1906388
• 负责人: Patricia Johann
• 金额: $ 51.08万
• 依托单位: Appalachian State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1906388&HistoricalAwards=false
• 关键词: SHF; Small; RUI; Semantic; Complexity

Testing of programs has dominated the last 50 years of software development, but the next 50 will see an increased demand for provably correct software. This is partly because modern applications are increasingly safety critical, partly because testing is by its very nature only a partial correctness guarantee, and partly because programming language technology is now at the stage where it is feasible to formally verify critical programs. Language-based verification uses a programming language's type system to help guarantee program correctness: the more program properties a type system can express, the more the compiler can automatically verify. Advanced data types such as Generalized Algebraic Data Types (GADTs) help close the so-called "semantic gap" between what programmers know about programs involving them and what a type system can express about those programs. The key observation underlying this project is that GADTs and other advanced data types are underspecified by their syntax, which often leads to them being used in unjustified ways that undermine their promise for verification. The project's novelty is a fully semantic response to this observation, embodied by the entirely novel notion of the functorial completion of a data type. This notion of functorial completion leads directly to the project's overall impact, which is to change the way programmers understand, and thus program with, GADTs and other advanced data types.The project shows that the way that even ordinary GADTs are currently understood is not formally justifiable and leads to unsafe programming practices, with the obvious consequences for verification, security, and reliability of software systems. It gives a grammar that generates a very general class of GADTs and other advanced data types, and uses the new notion of the functorial completion of a data type to give the data types generated by this grammar the same kind of semantics that has long been the cornerstone of the theory of standard algebraic data types. This ensures that data types generated by the grammar can be used with semantic and computational confidence. Furthermore it allows the data types to be classified according to semantic complexity--a novel notion introduced in this project--that helps programmers better understand a data type's semantic and computational properties. Finally, the project gives a framework for constructing parametric models for polymorphic languages supporting the advanced data types generated by the grammar. This framework is principled, conceptually simple, uniform, comprehensive, and predictive. It is constructed specifically to validate the semantics of the GADTs and other advanced data types generated by the grammar, and the constructs that are derived in a standard way from such semantics.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.

在过去50年的软件开发中，程序测试占据了主导地位，但在接下来的50年里，对可证明正确的软件的需求将会增加。这部分是因为现代应用程序对安全的要求越来越高，部分是因为测试本质上只是部分正确性保证，部分是因为编程语言技术现在处于正式验证关键程序是可行的阶段。基于语言的验证使用编程语言的类型系统来帮助保证程序的正确性：类型系统可以表达的程序属性越多，编译器可以自动验证的就越多。诸如通用代数数据类型(GADT)之类的高级数据类型有助于弥合程序员对涉及它们的程序的了解与类型系统对这些程序所能表达的信息之间的所谓“语义鸿沟”。这个项目背后的关键观察是，GADT和其他高级数据类型的语法规定不足，这往往导致它们被以不合理的方式使用，破坏了它们对验证的承诺。该项目的新颖性是对这一观察结果的完全语义响应，体现在数据类型的函数补全这一全新的概念中。这种功能完成的概念直接导致项目的整体影响，即改变程序员理解GADT和其他高级数据类型的方式。该项目表明，即使是普通的GADT目前被理解的方式也是不正当的，并导致不安全的编程实践，对软件系统的验证、安全和可靠性造成明显的后果。它给出了一种生成GADT和其他高级数据类型的非常通用的类的语法，并使用数据类型的函数补全的新概念来赋予由该语法生成的数据类型相同的语义，这种语义长期以来一直是标准代数数据类型理论的基石。这确保了语法生成的数据类型可以在语义和计算上可信地使用。此外，它允许根据语义复杂性对数据类型进行分类--这是本项目中引入的一个新概念--这有助于程序员更好地理解数据类型的语义和计算属性。最后，该项目给出了一个框架，用于构建支持由语法生成的高级数据类型的多态语言的参数模型。这一框架是原则性的，概念简单，统一，全面，具有预测性。它是专门为验证由语法生成的GADT和其他高级数据类型的语义，以及以标准方式从这些语义派生的构造而构建的。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

(Deep) Induction Rules for GADTs

GADT 的（深度）归纳规则

• DOI: 10.1145/3497775.3503680
• 发表时间: 2022
• 期刊: Certified Proofs and Programs
• 作者: Johann, Patricia;Ghiorzi, Enrico
• 通讯作者: Ghiorzi, Enrico

Parametricity for Primitive Nested Types

原始嵌套类型的参数化

• DOI: 10.26226/morressier.604907f41a80aac83ca25cb5
• 发表时间: 2021
• 期刊: Lecture notes in computer science
• 作者: Johann, P;Ghiorzi, E.;Jeffries, D.
• 通讯作者: Jeffries, D.

GADTs, Functoriality, Parametricity: Pick Two

GADT、函数性、参数性：选择两个

• 发表时间: 2021
• 期刊: Logical And Semantic Frameworks with Applications
• 作者: Johann, P.;Ghiorzi, E.;and Jeffries, D.
• 通讯作者: and Jeffries, D.

Partiality Wrecks GADTs’ Functoriality

偏向性破坏 GADT – 功能性

• 发表时间: 2023
• 期刊: TYPES
• 作者: Cagne, Pierre;Johann, Patricia
• 通讯作者: Johann, Patricia

Characterizing functions mappable over GADTs

表征可通过 GADT 映射的函数

• 发表时间: 2022
• 期刊: Asian Symposium on Programming Languages and Systems
• 作者: Johann, Patricia;Cagne, Pierre
• 通讯作者: Cagne, Pierre