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和其他高级数据类型被其语法指定，这通常会导致它们以不合理的方式使用，从而破坏了他们对验证的承诺。该项目的新颖性是对这一观察结果的完全语义响应，这是数据类型的功能完成的完全新颖的概念所体现的。该功能完成的概念直接导致了项目的整体影响，即改变程序员的理解方式，从而通过GADTS和其他高级数据类型进行编程。该项目表明，即使是普通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.

Characterizing functions mappable over GADTs

表征可通过 GADT 映射的函数

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

Partiality Wrecks GADTs’ Functoriality

偏向性破坏 GADT – 功能性

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